coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
*	Standardisation nom option_app en option_map	herbelin	2006-04-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Si un fixpoint a plusieurs arguments, mais un seul de type inductif,	letouzey	2006-04-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	ce patch dispense d'ecrire le { struct .. } En pratique, dans Topconstr.fixpoint_expr et Rawterm.fix_kind, l'index de l'argument inductif devient un int option au lieu d'un int. Les deux cas possibles: - Some n : les situations autorisées auparavant, a savoir {struct} explicite, ou bien un seul argument au total - None : le cas nouveau, qui redonne un entier lors du passage de rawconstr à constr si l'on trouve effectivement un unique argument ayant un type inductif, et une erreur sinon. Pour l'instant, on cherche l'inductif dans le type de manière syntaxique, mais il est jouable de rajouter un poil de reduction (au moins delta). Dans le détail, voici les coins que ce patch influence: - parsing/g_xml.ml4: continue pour l'instant a attendre un index explicite via un element xml "recIndex" - contrib/interface/xlate.ml: a priori ca marche, car il y avait déjà un cas ctv_ID_OPT_NONE correspondant à l'absence de struct. Par contre, dans le détail, le code pour un CFix utilise l'index de recurrence pour recouper au besoin le type du fixpoint en deux. Est-ce que je me gourre en supposant que si l'on a besoin de couper ainsi ce type, c'est qu'il provient non pas du parseur Coq, mais de l'impression d'un constr, et donc que l'index aura été correctement résolu ? - contrib/subtac/subtac_command.ml: - contrib/funind/indfun.ml: dans les deux cas, j'ai fait le service minimum, le struct reste obligatoire s'il y a plusieurs arguments. Mais ca ne serait pas dur à adapter pour ceux qui comprennent ces parties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8718 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes for new unification, not used in default version as it really changes ↵	msozeau	2006-04-10
\| \| \| \| \| \|	unification. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8695 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Actual fix for the unification problem in theories/Reals/Rtrigo_fun ↵	msozeau	2006-04-10
\| \| \| \| \| \| \| \| \| \| \|	(previous and current version work). Changed the type of typing constraints so as to have all the necessary information on abstract tycons. Updates of subtac to use the new type. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8693 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Documentation of the Program tactics.	msozeau	2006-04-07
\| \| \| \| \| \| \| \| \| \|	- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists. Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop. - Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Inductifs avec polymorphisme de sorte (version initiale)	herbelin	2006-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8673 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Subtac fixes, single fixpoint definitions are working again. Added a toggle ↵	msozeau	2006-03-22
\| \| \| \| \| \| \| \| \| \|	on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Made pretyping a functor over a coercion implementation. Pretyping.Default ↵	msozeau	2006-03-22
\| \| \| \| \| \| \| \| \| \| \|	uses the original Coercion implementation. Updated contributions that called pretyping to use the default impl. Also update subtac using the functor, do some renamings and add interfaces for all files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.	msozeau	2006-03-13
\| \| \| \| \| \| \| \|	May cause make world to fail because of dependency problems, make depend clean world should fix that (hopefully). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction message d'erreur ltac et adoption du modèle de message de Tacinterp	herbelin	2006-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8125 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation des erreurs de sorte du prétypage	herbelin	2006-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8011 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression résidus code v7 et traducteur	herbelin	2006-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des parseurs et printeurs v7; suppression du traducteur ↵	herbelin	2005-12-26
\| \| \| \| \| \|	(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration des points d'entrée de Pretyping et Constrintern	herbelin	2005-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7682 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
*	Nettoyage suite à la détection par défaut des variables inutilisées par ↵	herbelin	2005-11-08
\| \| \| \| \| \|	ocaml 3.09 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Types inductifs parametriques	mohring	2005-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Léger nettoyage et uniformisation + généralisation du point d'entrée ↵	herbelin	2005-09-09
\| \| \| \| \| \|	ltac pour qu'il retourne les evar git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparations de quelques petits bugs d\'unification + introduction de la ↵	barras	2005-06-07
\| \| \| \| \| \|	notion de variable de sortes (mais pas encore utilise... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7120 85f007b7-540e-0410-9357-904b9bb8a0f7
*	essai de typage des instantiations d\'evars	barras	2005-06-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur la substitution combinée avec l'instanciation en réponse à ↵	herbelin	2005-03-15
\| \| \| \| \| \|	l'inefficacité montrée dans le bug #932: suppression plutôt des Anonymous dans le contexte des evars (cf Evarutil) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	A défaut de substitution paresseuse ou explicite, ajout d'une substitution ↵	herbelin	2005-03-10
\| \| \| \| \| \|	optimisée pour le prétypage qui normalise les evars à la volée (cf bug #932) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6820 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Standardisation of function names about global references (especially, ↵	herbelin	2005-02-18
\| \| \| \| \| \|	renaming of constr_of_reference into constr_of_global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de la précédence des contexts de variables rel, ltac et var	herbelin	2005-02-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6660 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Relâchement obligation d'une contrainte de type sur les Hole en position ↵	herbelin	2004-12-06
\| \| \| \| \| \|	terminale, pour plus grande généralité de understand_gen_tcc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6421 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
*	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
*	Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵	herbelin	2004-08-24
\| \| \| \| \| \|	inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 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
*	correspondance des records et noms de champs de records entre un module et ↵	letouzey	2004-06-25
\| \| \| \| \| \|	sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte d'un type dont la sorte est une evar	herbelin	2004-04-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5710 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction incapacité à gérer les annotations de type dépendantes pour ↵	herbelin	2004-04-27
\| \| \| \| \| \|	le if-then-else git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5706 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2004-03-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5596 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵	herbelin	2004-03-28
\| \| \| \| \| \|	sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modif des fixpoints pour que si on donne une notation au produit, les pts ↵	barras	2004-03-05
\| \| \| \| \| \|	fixes s'affichent correctement git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Localisation un tout petit peu moins abstraite des erreurs de garde, mais ↵	herbelin	2004-02-04
\| \| \| \| \| \|	reste a transporter les loc dans check_fix git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5292 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur recuperation de noms a partir du type, car casse la correction ↵	herbelin	2004-02-03
\| \| \| \| \| \|	des dependances de nom git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5283 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation d'une rupture (en presence de types implicites) de l'invariant ↵	herbelin	2004-01-29
\| \| \| \| \| \|	que les variables liees sont toujours nommees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Substitution dans REvar et PEvar plutot que encodage via noeud application ↵	herbelin	2003-12-19
\| \| \| \| \| \|	pour eviter la confusion avec la (vraie) application git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Deplacement subst_rawconstr dans Rawterm	herbelin	2003-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4948 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration message d'erreur pour ltac	herbelin	2003-11-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Oubli du type du terme a filtrer quand pas d'argument dans la traduction de case	herbelin	2003-09-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement de l'afficheur pour que les variables liées aient un nom ↵	herbelin	2003-09-23
\| \| \| \| \| \|	indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug predicat old Case	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4345 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug predicat let-tuple	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4338 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout construction If primitive dans constr_expr et rawconstr	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4336 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug et améliorations diverses	herbelin	2003-08-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4264 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7