coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	maj	coq	2005-01-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6556 85f007b7-540e-0410-9357-904b9bb8a0f7
*	HUGE COMMIT	sacerdot	2005-01-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	1. when applying a functor F(X) := B to a module M, the obtained module is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the body of t in M}. In principle it is now easy to fine tune the behaviour to choose whether b or M.t must be used. This change implies modifications both inside and outside the kernel. 2. for each object in the library it is now necessary to define the behaviour w.r.t. the substitution {X.t := b}. Notice that in many many cases the pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken (in the sense that it used to break several invariants). This commit fixes the behaviours for most of the objects, excluded a) coercions: a future commit should allow any term to be declared as a coercion; moreover the invariant that just a coercion path exists between two classes will be broken by the instantiation. b) global references when used as arguments of a few tactics/commands In all the other cases the behaviour implemented is the one that looks to me as the one expected by the user (if possible): [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ] a) argument scopes: not expanded b) SYNTAXCONSTANT: expanded c) implicit arguments: not expanded d) coercions: expansion to be done (for now not expanded) e) concrete syntax tree for patterns: expanded f) concrete syntax tree for raw terms: expanded g) evaluable references (used by unfold, delta expansion, etc.): not expanded h) auto's hints: expanded when possible (i.e. when the expansion of the head of the pattern is rigid) i) realizers (for program extraction): nothing is done since the actual code does not look for the realizer of definitions with a body; however this solution is fragile. l) syntax and notation: expanded m) structures and canonical structures: an invariant says that no parameter can happear in them ==> the substitution always yelds the original term n) stuff related to V7 syntax: since this part of the code is doomed to disappear, I have made no effort to fix a reasonable semantics; not expanded is the default one applied o) RefArgTypes: to be understood. For now a warning is issued whether expanded != not expanded, and the not expanded solution is chosen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2005-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6551 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2005-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6547 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6527 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-24
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6429 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Names.substitution (and related functions) and Term.subst_mps moved to	sacerdot	2004-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
*	maj	filliatr	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6246 85f007b7-540e-0410-9357-904b9bb8a0f7
*	COMMITED BYTECODE COMPILER	barras	2004-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-10-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6239 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6229 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-10-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6181 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6146 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-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:	sacerdot	2004-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
*	maj	filliatr	2004-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 deps	barras	2004-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-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 parsing	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
*	repaired deps	barras	2004-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6112 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-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_defs	barras	2004-09-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6106 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6100 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6086 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-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 fonctionnel	barras	2004-09-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6068 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6059 85f007b7-540e-0410-9357-904b9bb8a0f7
*	deplacement de clenv vers pretyping	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
*	premiere reorganisation de l\'unification	barras	2004-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-08-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-07-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5976 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-07-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-07-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-07-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5959 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5933 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-07-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5878 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-06-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5858 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5854 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moved instantiate binding to extratactics	corbinea	2004-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2004-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	more evar stuff	corbinea	2004-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5843 85f007b7-540e-0410-9357-904b9bb8a0f7