coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Uniformisation politique de nommage evd/isevars (evd si evar_defs,	herbelin	2007-09-06
\| \| \| \| \| \| \|	evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Le calcul de la classe dans class_args_of ne suivait pas celui de class_of	herbelin	2006-10-21
\| \| \| \| \| \| \| \|	(avec comme conséquence des échecs en cas de beta-redex - cf coercions.v). Allègements triviaux dans coercion.ml en passant. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction d'un vieux bug de coercion avec éta-expansion (utilisation	herbelin	2006-10-21
\| \| \| \| \| \| \|	de subst1 au lieu de subst_term). Indentation plus compacte au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9255 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement des nf_evar (source de complexité polynomiale) par de la	herbelin	2006-10-06
\| \| \| \| \| \| \| \| \| \| \| \|	réduction paresseuse. Accessoirement, suppression d'un test evar_defined inutile car sur résultat de whd_betadeltaiota qui contient la réduction evar de tête dans coercion.ml; code mort du commit précédent dans pretyping.ml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9223 85f007b7-540e-0410-9357-904b9bb8a0f7
*	The "clean integration of subtac" patch.	msozeau	2006-05-29
\| \| \| \| \| \| \| \| \| \| \| \| \|	Adds a new kind of casts (CastCoerce) for coercing an object to its base type (e.g. inductive). The new cast_type type subsumes usual casts ConvCasts. Much of the patch is just adding ConvCasts where needed. The Pretyping module has been adapted to this change, although it doesn't change anything yet, but this construct could have a use with current coercions also. Pretyping is also cleaned from the "Use type constraints under lambdas" patch which is not yet ready for wide use. It has been transferred to a copy of the Pretyping Functor in subtac_pretyping_F.ml. Subtac is now working as well as I demonstrated at TYPES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8875 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
*	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
*	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
*	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
*	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
*	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
*	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
*	Deuxième passe sur la localisation des messages d'erreurs sur les evars non ↵	herbelin	2002-04-11
\| \| \| \| \| \|	définies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place de coercion dans les motifs	herbelin	2001-12-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2285 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
*	L'instantiation des evars quand un produit ou une sorte étaient attendus ↵	herbelin	2001-09-14
\| \| \| \| \| \|	n'était pas fait git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1966 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug de Bruijn	herbelin	2001-08-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1896 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration des messages d'erreurs vis a vis des evars	barras	2001-05-23
\| \| \| \| \| \| \|	ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amelioration de la structure des univers	barras	2001-03-28
\| \| \| \| \| \| \| \|	elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	entetes	filliatr	2001-03-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration de classops; évolution en une version mieux intégrée au ↵	herbelin	2001-02-05
\| \| \| \| \| \|	reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1329 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug environnement	herbelin	2001-01-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1242 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Insertion de coercion au milieu des applications partielles et propagation ↵	herbelin	2000-11-08
\| \| \| \| \| \|	des contraintes de prétypage vers les sous-termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des (* open Generic *)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petit nettoyage de Evarutil et Evarconv	herbelin	2000-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@735 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage Coercion	herbelin	2000-10-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simplifications autour de typed_type (renommé types par analogie avec ↵	herbelin	2000-10-18
\| \| \| \| \| \|	sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage canonique :	herbelin	2000-10-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	declaration = definition \| assumption mode de reference = named \| rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifierconstrtyped_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage AppL en App	herbelin	2000-10-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@634 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction de constr	herbelin	2000-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@604 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification mkAppL; abstraction via kind_of_term; changement dans Reduction	herbelin	2000-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction pour make doc	herbelin	2000-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@594 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un LetIn primitif.	herbelin	2000-09-10
\| \| \| \| \| \| \|	Abstraction de constr via kind_of_constr dans une bonne partie du code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@591 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage à des contextes de vars et de rels pouvant contenir des déclarations	herbelin	2000-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Achèvement abstraction du mécanisme (optionnel) de cast	herbelin	2000-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amelioration messages erreurs	herbelin	2000-06-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs et simplification (suite)	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs et simplifications coercions	herbelin	2000-06-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'un choix constr/typed_type en remplacement de certains Cast	herbelin	2000-06-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Afficahge des locations	herbelin	2000-05-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modification messages d'erreurs, possibilité de n'importe quel constr dans ↵	herbelin	2000-05-26
\| \| \| \| \| \|	les instances de références git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Abstraction du type typed_type (un pas vers les jugements 2 niveaux)	herbelin	2000-04-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@362 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export inh_conv_coerce_to et divers	herbelin	2000-03-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@298 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros commit de tout ce que j'ai fait pendant les vacances :	filliatr	2000-01-21
\| \| \| \| \| \| \| \| \| \|	- tactics/Equality - debug du discharge - constr_of_compattern implante vite fait / mal fait en attendant mieux - theories/Logic (ne passe pas entierrement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@280 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- méthode load sur les Hints	filliatr	1999-12-13
\| \| \| \| \| \| \| \|	- CAST pris en compte dans Astterm - Coercin.lookup_path_to_sort_from protégé par un try/with git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour Coercion	filliatr	1999-12-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@172 85f007b7-540e-0410-9357-904b9bb8a0f7