coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adding the tactic "instantiate" (without argument), to force the	glondu	2007-12-07
\| \| \| \| \| \| \|	instantiation of evars in tacticals (cf r9985, r10294). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10356 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension to the general sequence operator (tactical). Now in addition to ↵	emakarov	2007-04-02
\| \| \| \| \| \| \| \| \| \| \|	the form expr_0 ; [ expr_1 \| ... \| expr_n ] where expr_i could be empty, expr_i may be ".." or "expr ..". Note that "..." is a part of the metasyntax while ".." is a part of the object syntax. It may be necessary to enclose expr in parentheses. There may be at most one expr_i ending with "..". The number of expr_j not ending with ".." must be less than or equal to the number of subgoals generated by expr_0. The idea is that if expr_i is "expr .." or "..", then the value of expr (or idtac in case "..") is applied to as many intermediate subgoals as necessary to make the number of tactics equal to the number of subgoals. More precisely, if expr_0 generates n subgoals then the command expr_0; [expr_1 \| ... \| expr_i .. \| ... \| expr_m], where 1 <= i <= m, applies (the values of) expr_1, ..., expr_{i-1} to the first i - 1 subgoals, expr_i to the next n - m + 1 subgoals, and expr_{i+1}, ..., expr_m to the last m - i subgoals. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9742 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction du bug #1315:	notin	2007-01-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- ajouts des opérations clear_evar_hyps_in_evar, clear_evar_hyps_in_constr et clear_evar_hyps dans Evarutil, qui permettent de supprimer des hypothèses dans le contexte des evars, en créant une nouvelle evar avec un contexte restreint; - adaptation de clear_hyps dans Logic pour qu'elle mette à jour le contexte des evars; - adaptation de prim_refiner pour qu'elle renvoie le evar_map modifié; - déplacement de la tactique Change_evars dans prim_rule. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug #1194: normalisation evars a la sortie de focus	barras	2006-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9261 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage des ... dans les scripts	barras	2006-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9244 85f007b7-540e-0410-9357-904b9bb8a0f7
*	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey	2006-10-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9211 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras	2006-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9178 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Declarative Proof Language: main commit	corbinea	2006-09-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	replacing whd_betaiotaevar_preserving_vm_cast	jforest	2006-04-14
\| \| \| \| \| \| \|	by nf_betaiotaevar_preserving_vm_cast. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8708 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8107 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ↵	herbelin	2006-01-21
\| \| \| \| \| \|	et variables ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7911 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement d'egalite pour le named_context_val	gregoire	2005-12-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7640 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des named_context	gregoire	2005-12-02
\| \| \| \| \| \| \| \|	Ajout de cast indiquant au kernel la strategie a suivre Resolution du bug sur les coinductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Confusion assert/error détectée par nouveau warning X de ocaml 3.09	herbelin	2005-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) (continued!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6975 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection against saving a proof with still non-instantiated evars (cf bug ↵	herbelin	2005-04-29
\| \| \| \| \| \|	#901) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6974 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵	herbelin	2004-12-31
\| \| \| \| \| \|	Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en page	herbelin	2004-11-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6322 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
*	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
*	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
*	Nouvelle en-tête	herbelin	2004-07-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
*	added breakpoints to help ide	corbinea	2004-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5387 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage des metas dans un environnement avec definitions locales (bug 277)	herbelin	2003-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5116 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Idtac peut prendre un argument à afficher	narboux	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	2 espaces en trop	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4812 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration de l'afficheur de script structure	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4797 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground update	corbinea	2003-07-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4227 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ground Update.	corbinea	2003-06-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4188 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des tactiques en v8	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3865 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un message à FailTac	herbelin	2003-03-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Option pour rendre les vérifications du refiner optionnelle	herbelin	2002-12-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3400 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intégration des modifs de la branche mowgli :	herbelin	2002-11-05
\| \| \| \| \| \| \| \| \| \| \|	- Simplification de strength qui est maintenant un simple drapeau Local/Global. - Export des catégories de déclarations (Lemma/Theorem/Definition/.../ Axiom/Parameter/..) vers les .vo (nouveau fichier library/decl_kinds.ml). - Export des variables de section initialement associées à une déclaration (nouveau fichier library/dischargedhypsmap.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3212 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre l'encapsulage de FailError dans Exc_located (sinon, par ↵	herbelin	2002-07-11
\| \| \| \| \| \|	exemple, 'Try Tauto' ne marche pas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2855 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation des tclTHEN (cf dev/changements.txt)	herbelin	2002-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2721 85f007b7-540e-0410-9357-904b9bb8a0f7
*	prterm -> prterm_env	filliatr	2002-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	compat ocaml 3.03	filliatr	2001-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de l'affichage des noeuds Change_evars	barras	2001-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2289 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des stamps et donc des *_constraints	clrenard	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2186 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suites modifs du noyau. Univ devient purement fonctionnel.	barras	2001-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des local_constraints, des ctxtty et du focus.	clrenard	2001-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2163 85f007b7-540e-0410-9357-904b9bb8a0f7
*	GROS COMMIT:	barras	2001-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