aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
Commit message (Collapse)AuthorAge
* entetesGravatar filliatr2001-03-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
* Erreur sur commitGravatar herbelin2001-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1389 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un système optionnel de discharge immédiat; prise en ↵Gravatar herbelin2001-02-14
| | | | | | compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ré-introduction des implicites à la volée dans la définition des inductifsGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1279 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des noms longs dans les Hints et les Coercions, et ↵Gravatar herbelin2001-01-24
| | | | | | réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réorganisation suite ajout de constantes locales dans les RecordsGravatar herbelin2001-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rattrapage d'erreur pour le Case + Eval Compute in pour DefinitionGravatar delahaye2001-01-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1232 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout du Let pour le langage de tactiquesGravatar delahaye2000-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1231 85f007b7-540e-0410-9357-904b9bb8a0f7
* Découpage des différentes fonctionnalités de build_mutual et ↵Gravatar herbelin2000-12-19
| | | | | | definition_structure + export des sous-fonctions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1155 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug des locaux au premier niveau des modules qui disparaissaient de ↵Gravatar herbelin2000-12-15
| | | | | | l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les params d'inductif deviennent en même temps propre à chaque inductif ↵Gravatar herbelin2000-12-14
| | | | | | d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
* caractere opaque des constantes repris en compteGravatar filliatr2000-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1045 85f007b7-540e-0410-9357-904b9bb8a0f7
* Distinction local/globalGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Branchement des Local sur des SectionLocalDefGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@977 85f007b7-540e-0410-9357-904b9bb8a0f7
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2000-11-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique SectionLocalDecl -> SectionLocalAssumGravatar herbelin2000-11-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵Gravatar filliatr2000-11-06
| | | | | | constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2000-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@742 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifications autour de typed_type (renommé types par analogie avec ↵Gravatar herbelin2000-10-18
| | | | | | sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique :Gravatar herbelin2000-10-18
| | | | | | | | | | | | | | declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage AppL en AppGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@635 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@618 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de constrGravatar herbelin2000-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction pour make docGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un LetIn primitif.Gravatar herbelin2000-09-10
| | | | | | | Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Canonisation de certains noms dans Pretyping, Asterm et Safe_typingGravatar herbelin2000-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage à des contextes de vars et de rels pouvant contenir des déclarationsGravatar herbelin2000-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug: on tentait de déclarer un schéma d'induction pour un coinductifGravatar herbelin2000-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de GenericGravatar herbelin2000-05-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de save_thm and co de PFedit vers CommandGravatar herbelin2000-05-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@477 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suite restructuration inductifs; changement nom module Constant en DeclarationsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@458 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface de PfeditGravatar herbelin2000-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type typed_type (un pas vers les jugements 2 niveaux)Gravatar herbelin2000-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage de l'interface d'Astterm; renommage des constr_of_com and co en ↵Gravatar herbelin2000-03-28
| | | | | | interp_constr etc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@356 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réparation du cast oublié lors d'une définition castéeGravatar herbelin2000-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@305 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage des fichiers de parsingGravatar herbelin2000-01-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@277 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de RecordGravatar herbelin2000-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@275 85f007b7-540e-0410-9357-904b9bb8a0f7
* message erreur SchemeGravatar herbelin1999-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@259 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux types 'constructor' et 'inductive' dans Term;Gravatar herbelin1999-12-15
| | | | | | | | | les fonctions sur les inductifs prennent maintenant des 'inductive' en paramètres; elle n'ont plus besoin de faire des appels dangereux aux find_m*type qui centralisent la levée de raise Induc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les inductifs dans Scheme doivent être des ident d'inductifsGravatar herbelin1999-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@256 85f007b7-540e-0410-9357-904b9bb8a0f7
* petite erreur dans CommandGravatar filliatr1999-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@246 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentation interfacesGravatar filliatr1999-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@244 85f007b7-540e-0410-9357-904b9bb8a0f7
* modulesGravatar filliatr1999-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@238 85f007b7-540e-0410-9357-904b9bb8a0f7
* - constantes avec recettesGravatar filliatr1999-12-09
| | | | | | | | - discharge en deux temps, avec état remis comme au début de la section (mais c'est toujours buggé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@224 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement de Discharge dans toplevelGravatar filliatr1999-12-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@222 85f007b7-540e-0410-9357-904b9bb8a0f7
* declarations eliminations / debuggae inductifs (debut)Gravatar filliatr1999-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@212 85f007b7-540e-0410-9357-904b9bb8a0f7
* premier debugageGravatar filliatr1999-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@210 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 16:00:42 +0000