aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/sign.mli
Commit message (Collapse)AuthorAge
* Merging Context and Sign.Gravatar ppedrot2013-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16463 85f007b7-540e-0410-9357-904b9bb8a0f7
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
| | | | | | | | | | | | | | | | | 1. sorts.ml: A small file utility for sorts; 2. constr.ml: Really low-level terms, essentially kind_of_constr, smart constructor and basic operators; 3. vars.ml: Everything related to term variables, that is, occurences and substitution; 4. context.ml: Rel/Named context and all that; 5. term.ml: derived utility operations on terms; also includes constr.ml up to some renaming, and acts as a compatibility layer, to be deprecated. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16462 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modulification of identifierGravatar ppedrot2012-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updating headers.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
* Environ: generic equality on named_context replaced by named_context_equalGravatar puech2011-07-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
| | | | | | Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
| | | | | | | | | | | - Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
| | | | | | | | | | | | | | | | | | | dev/ocamlweb-doc has been erased. I hope no one still use the "new-parse" it generate. In dev/, make html will generate in dev/html/ "clickable version of mlis". (as the caml standard library) make coq.pdf will generate nearly the same awfull stuff that coq.ps was. make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of the given directory. ocamldoc comment syntax is here : http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html The possibility to put graphs in pdf/html seems to be lost. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
| | | | | | | | | | splay_prod_n, lam_it -> it_mkLambda, splay_lambda -> splay_lam). Added shortcuts for "fst (decompose_prod t)" and co. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout iter_rel_context/iter_named_contextGravatar herbelin2006-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added map_named_contextGravatar herbelin2005-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6737 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)Gravatar barras2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution du pb d'efficacite du a Sign.add_named_declGravatar barras2002-04-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2610 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression de pop_namedGravatar barras2002-02-22
| | | | | | | meilleure discrimination dans les tactiques d'inversion git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Reforme de la gestion des args recursifs (via arbres reguliers)Gravatar barras2002-02-14
| | | | | | | - coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout mkArityGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2218 85f007b7-540e-0410-9357-904b9bb8a0f7
* types vs constrGravatar herbelin2001-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suites modifs du noyau. Univ devient purement fonctionnel.Gravatar barras2001-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
* GROS COMMIT:Gravatar barras2001-11-05
| | | | | | | | | | - reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression des arguments sur les constantes, inductifs et constructeursGravatar barras2001-10-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
* 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
* Prise en compte des let in dans les instances de globauxGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@976 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
* 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
* 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@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
* Renommage hypothèses de nom redondant dans les environnementsGravatar herbelin2000-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@465 85f007b7-540e-0410-9357-904b9bb8a0f7
* docGravatar herbelin2000-05-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@427 85f007b7-540e-0410-9357-904b9bb8a0f7
* Sign.db_signature is now an abstract typeGravatar courant2000-04-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@364 85f007b7-540e-0410-9357-904b9bb8a0f7
* documentationGravatar filliatr2000-01-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
* erreurs latex dans interfacesGravatar filliatr2000-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@287 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ ocaml 2.99 (espaces dans la syntaxe des cast)Gravatar herbelin2000-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@284 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction de l'implémentation des signatures de Sign en vue intégration ↵Gravatar herbelin2000-01-26
| | | | | | du let-in git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 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
* ajouts divers pour module PrinterGravatar filliatr1999-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@145 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ pour fusion avec pretypingGravatar herbelin1999-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
* - un effort sur la doc (ocamlweb)Gravatar filliatr1999-09-19
| | | | | | | | | - module Nametab - module Impargs - correction bug : Parameter id : t => vérification que t est bien un type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 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
* environnement surGravatar filliatr1999-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@28 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 06:34:28 +0000