aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.mli
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
* 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
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameGravatar herbelin2000-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1141 85f007b7-540e-0410-9357-904b9bb8a0f7
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au ↵Gravatar herbelin2000-11-27
| | | | | | evaluable_constant qui change de type au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout push_rels_assumGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout sp_of_global; Introduction constant_path = section_pathGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@875 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
* 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
* 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
* Ajout push_rec_typesGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@695 85f007b7-540e-0410-9357-904b9bb8a0f7
* Elimination des coupures sur le type constantGravatar herbelin2000-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rebranchement de la tactique LetGravatar herbelin2000-10-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@638 85f007b7-540e-0410-9357-904b9bb8a0f7
* Disparition du type oper mais nouveau type global_referenceGravatar herbelin2000-10-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@620 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
* nettoyageGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@595 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression de AbstGravatar herbelin2000-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 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@591 85f007b7-540e-0410-9357-904b9bb8a0f7
* retablissement make doc et make minicoqGravatar filliatr2000-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 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
* Mise en place d'un choix constr/typed_type en remplacement de certains CastGravatar herbelin2000-06-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 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
* Centralisation prod_name and co dans Environ; mkLambda_string dans TermGravatar herbelin2000-05-18
| | | | | | | Effets de bords suite à la restructuration des inductives (cf Inductive) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@441 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout {prod,lambda}_nameGravatar herbelin2000-03-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@349 85f007b7-540e-0410-9357-904b9bb8a0f7
* TautoGravatar filliatr2000-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@331 85f007b7-540e-0410-9357-904b9bb8a0f7
* gros commit de tout ce que j'ai fait pendant les vacances :Gravatar filliatr2000-01-21
| | | | | | | | | | - tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 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
* Poursuite intégration du CasesGravatar herbelin1999-12-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@242 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des messages d'erreurs de CasesGravatar herbelin1999-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@226 85f007b7-540e-0410-9357-904b9bb8a0f7
* - environment -> safe_environmentGravatar filliatr1999-12-01
| | | | | | | - unsafe_env -> env git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@168 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Typing -> Safe_typingGravatar filliatr1999-12-01
| | | | | | | | | - proofs/Typing_ev -> pretyping/Typing - env -> sign - fonctions var_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@167 85f007b7-540e-0410-9357-904b9bb8a0f7
* les variables existentielles contiennent maintenant un environnement (typeGravatar filliatr1999-10-19
| | | | | | | | unsafe_env) et non pas seulement une signature. Le module Evd vient donc apres le module Environ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@108 85f007b7-540e-0410-9357-904b9bb8a0f7
* - déplacement (encore une fois !) des variables existentielles : elles sontGravatar filliatr1999-10-18
| | | | | | | | | | toujours dans le noyau (en ce sens que Reduction et Typeops les connaissent) mais dans un argument supplémentaire A COTE de l'environnement (de type unsafe_env) - Indtypes et Typing n'utilisent strictement que Evd.empty git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@106 85f007b7-540e-0410-9357-904b9bb8a0f7
* module LogicGravatar filliatr1999-10-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@105 85f007b7-540e-0410-9357-904b9bb8a0f7
* - re-introduction d'une evar_map dans unsafe_envGravatar filliatr1999-10-13
| | | | | | | - les var. ex. sont des entiers, et non plus des section_path git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@99 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacements des var. ex. hors du noyauGravatar filliatr1999-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7
* ensembles de contraintes d'universGravatar filliatr1999-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@78 85f007b7-540e-0410-9357-904b9bb8a0f7
* mise en place repertoire test-suite/, toplevel/, parsing/Gravatar filliatr1999-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@39 85f007b7-540e-0410-9357-904b9bb8a0f7
* - environnements videsGravatar filliatr1999-09-03
| | | | | | | | - suppression du constructeur Implicit (et IsImplicit du coup) - nettoyages divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@35 85f007b7-540e-0410-9357-904b9bb8a0f7
* un petit effort de presentation dans les interfacesGravatar filliatr1999-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression champs inutiles dans constantes et inductifs; verification ↵Gravatar filliatr1999-08-27
| | | | | | definitions inductives git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@29 85f007b7-540e-0410-9357-904b9bb8a0f7
* environnement surGravatar filliatr1999-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 85f007b7-540e-0410-9357-904b9bb8a0f7
* modules Instantiate, Constant et InductiveGravatar filliatr1999-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@22 85f007b7-540e-0410-9357-904b9bb8a0f7
* mach et himsg; typage sans extractionGravatar filliatr1999-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@21 85f007b7-540e-0410-9357-904b9bb8a0f7
* machine: execute = typage avec universGravatar filliatr1999-08-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@18 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Reduction (fin)Gravatar filliatr1999-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14 85f007b7-540e-0410-9357-904b9bb8a0f7
* module Reduction (debut)Gravatar filliatr1999-08-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12 85f007b7-540e-0410-9357-904b9bb8a0f7
* module ClosureGravatar filliatr1999-08-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 14:38:52 +0000