aboutsummaryrefslogtreecommitdiffhomepage
path: root/.depend
Commit message (Collapse)AuthorAge
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
| | | | | | | | | | | the new module kernel/mod_subst.ml. MOTIVATION: mod_subst is compiled after kernel/term.ml; thus it is now possible to define substitutions that also delta-expand constants (by associating the delta-expanded form to the constant name). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6304 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6246 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6239 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-10-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6229 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6223 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6181 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6146 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6130 85f007b7-540e-0410-9357-904b9bb8a0f7
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
| | | | | | | | | | | | | | "Add Morphism m @ arg1 ... argn @ out as ident" where argi = constr arrow and arrow = "-->" | "++>" | "==>" (for contravariant, covariant and bi-variant morphisms). The syntax should be improved by getting rid of the "@" and maybe choosing better symbols to represent the arrows. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6129 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6120 85f007b7-540e-0410-9357-904b9bb8a0f7
* pbs with link order and depsGravatar barras2004-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6116 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6114 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
* repaired depsGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6112 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6110 85f007b7-540e-0410-9357-904b9bb8a0f7
* hiding the meta_map in evar_defsGravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6106 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6100 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6097 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6086 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6072 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6068 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6059 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement de clenv vers pretypingGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5976 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5974 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5963 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5959 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5933 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5878 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5858 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5854 85f007b7-540e-0410-9357-904b9bb8a0f7
* moved instantiate binding to extratacticsGravatar corbinea2004-06-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5845 85f007b7-540e-0410-9357-904b9bb8a0f7
* more evar stuffGravatar corbinea2004-06-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5834 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5800 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-05-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5728 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5693 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj annonce depuis la v8beta vers v8Gravatar narboux2004-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5690 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5659 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5631 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5625 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5606 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5594 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5582 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 13:32:38 +0000