aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2005-04-21Gestion du forall et envoie d'axiome à la procédurecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6950 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-07dp: traitement des definitionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6919 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-04-05Problemes de renommage reglescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6914 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-24symboles de fonctions globaux traitescoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6882 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-22Ajout de l'axiome du but prouve par la tactique simplificoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6875 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-18appel de Simplify depuis Coqcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6854 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16tactiques prouveurs premier ordre dans contrib/dp/coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6842 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-16nouvelles tactiques pour appeler des procedures de decision du premier ordrecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6841 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-15Unsharing before exportation to ensure uniqueness of xml id'sherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6837 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-03-07Added 'clear - id' to clear all hypotheses except the ones dependent in the ↵herbelin
statement of id git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21Pas de dépendance en Omegaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6764 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21Correction de bugs: coq_false et coq_true au lieu de coq_False et coq_trueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6763 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21- changement ordre arguments interp_goal_concl pour permettre applicationherbelin
partielle - amélioration traduction en nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6762 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-21- Correction de bugsherbelin
- filtrage sur Bigint.zero incorrect: zero était considéré comme une variable - coq_false et coq_true au lieu de coq_False et coq_true - vérification chargement ROmega.vo - Divers - changement ordre argument interp_goal_concl pour permettre application partielle - amélioration débogueur - ajout interprétation Zsucc, Zopp, et gel de Zmult si non scalaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6761 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Renaming Print Canonical Structure into Print Canonical Projectionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6750 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6746 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-18Standardisation of function names about global references (especially, ↵herbelin
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
2005-02-18Déboggueur et code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6742 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-17Correction bug #922 (problème dans depend) + formattage débogueurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6727 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Uniformisation de destApplication en destAppherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6713 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-12Ajout Print Canonical Structuresherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6711 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-06Nettoyage et documentation de Libraryherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Ajout printer direct cic vers xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6682 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-04Export du printer xml vers tacinterpherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6681 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Implemented a test for "Add [Semi] Setoid Ring" to check that the givensacerdot
compatibility proofs are the default compatibility proofs for their respective operation. This closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6668 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-03Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"sacerdot
prevendent detection of only one mistake in the user input. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6667 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02The statement of the compatibility theorem for addition and multiplicationsacerdot
have been changed to match the new statement used by Add Setoid. NOTE: this reveals a missing check in the code. Indeed, "Add Setoid Ring" does not check if the provided compatibility theorems have the expected type. To be done in a future commit. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6662 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-02-02 setoid_rewrite t; [tac]sacerdot
now used in place of setoid_replace ... with ... ; try (exact t) ; tac The new stricter version closes a bug reported by Pierre Letouzey on coqdev. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6661 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-26Ajout cas VernacBackToherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-14Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedsacerdot
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body) instead of looking it up in the environment. A version of the same functions with the old type is put in Inductiveops (outside the kernel). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
"T with (Definition|Module) M1.M2....Mn.id := c" (in the ML style). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6582 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-06- Module/Declare Module syntax made more uniform:sacerdot
* "Module X [binders] [:T] [:= b]." is now used to define a module both in module definitions and module type definitions. Moreover "b" can now be a functor application in every situation (this was not accepted for module definitions in module type definitions) * "Declare Module X : T." is now used to declare a module both in module definitions and module type definitions. - Added syntactic sugar "Declare Module Export/Import" and "Module Export/Import" - Added syntactic sugar "Module M(Export/Import X Y: T)" and "Module Type M(Export/Import X Y: T)" (only for interactive definitions) (doc TODO) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6564 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-03HUGE COMMITsacerdot
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
2005-01-02Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵herbelin
dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-01-01Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵herbelin
Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6541 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-29Bug transformation assert dans commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6522 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-27Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-27Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise ↵herbelin
par romega (omega2.ml, qui, l'occassion, disparat sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-24Passage d'une bibliothèque de grands entiers naturels vers une ↵herbelin
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@6501 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-10Hugo fixed a bug of refine, and it revealed a bug of functionalcoq
induction. Some metas were left in the type of metas of the term given to refine by functional induction. This commit fixes this bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6462 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Restauration type casted_open_constr pour tactique refine car l'unification ↵herbelin
n'est pas assez puissante pour retarder la coercion vers le but au dernier moment git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6458 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09travail sur les types extraitsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-07* added subst_evaluable_referencesacerdot
* the Unfold hints of auto/eauto now use evaluable_global_references in place of global_references git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6428 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵herbelin
tactiques d'appliquer une éventuelle coercion vers le but git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6408 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Orthographe!herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6395 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Correction 1.138 appliquée à tort à la branche principale au lieu de ↵herbelin
V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Commit précédent erroné; retour version précédenteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-28MAJ vis à vis de extratacticsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-18When a reference to a constructor is met its inductive type must be closed.sacerdot
This commit fixes the bug that prevented extraction of Lyon/CIRCUITS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6328 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 23:13:18 +0000