coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Orthographe de 'instantiate'	herbelin	2005-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added clenv_environments_evars that behaves as clen_environments but	sacerdot	2005-05-24
\| \| \| \| \| \| \| \| \|	generating evars in place of metas. Notice that thanks to this changement unification can be more effective (expecially after reduction) since evars have non-empty contexts whereas metas have not. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7069 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A wish by Bas Spitters granted: a little more of unification up to	sacerdot	2005-05-19
\| \| \| \| \| \| \| \|	convertibility is now tried in setoid_rewrite. As a consequence it is now possible to declare relations over the function space (fun A B: Type => A -> B). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7039 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilité ocamlweb pour cible doc	herbelin	2005-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 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
*	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
*	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
*	inclusion de meta_map dans evar_defs	barras	2004-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification de clenv	barras	2004-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
*	unification encore...	barras	2004-09-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 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
*	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