Sections:
- type déclaré: quantification polymorphe sur les lemmes et les opérateurs
    * module type et module global ne peut pas utiliser type déclaré.
- type local:
	* alias inlinés (restrictions héritées du caractere déclaré de sa définition);
	* non-alias ne peuvent apparaitre que dans des bidouillons locaux.

- opérateur declaré: quantification universelle, opérateurs monomorphes (ou utilisés de maniere parametrique, mais ca n'a pas l'air tres utile)
	* ne peut pas apparaitre dans un module global
- opérateur local:
	* non-inductifs (alias) inlinés (restrictions héritées du caractere déclaré de sa définition);
	* inductifs (point fixe) ne peut apparaitre que dans des bidouillons locaux.

- module type déclaré: inutile?
- module type local: ne peut apparaitre que dans des bidouillons locaux.

- module déclaré: quantification sur les lemmes.
	* module global ne peut pas utiliser module déclaré.
- modules locaux:
	* alias inlinés (restrictions héritées du caractere déclaré de sa définition);
	* non-alias ne peuvent apparaitre que dans des bidouillons locaux.

- axiome:
	* par défaut: prémisse dans les lemmes;
	* global axiom: ne peut parler que de choses globales, exportés par la section.

Clones: on calcule le clone final a partir de la chaine de clones et on l'applique a la théorie de base
- type, op, module:
	* abstrait: facile
	* concret: convertibilité
- axiom, lemme:
	* une fois le lemme prouvé, le reprouver donne une erreur;
	* l'étoile capture tous les axiomes qui n'ont pas déja été prouvés;
	* quand l'instance arrive avec une preuve pour le lemme , on n'envoie pas sa nouvelle copie.

Clone in sections:
- quand on instancie une entité par un corps qui a des symboles declarés, toutes les entités qui en dépendent doivent etre locales,
- Sucre:
  - on veut pouvoir marquer local une expression de clone (clone local), ou une instruction de clone (with local op x <- ...),
		* s'il ne reste rien d'une théorie apres un clone local, on la vire completement.
  - on veut pouvoir marquer declare une instruction de clone (with declare op x).