aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
Commit message (Collapse)AuthorAge
* Implemented a test for "Add [Semi] Setoid Ring" to check that the givenGravatar sacerdot2005-02-03
| | | | | | | | 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
* Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"Gravatar sacerdot2005-02-03
| | | | | | | 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
* The statement of the compatibility theorem for addition and multiplicationGravatar sacerdot2005-02-02
| | | | | | | | | | | 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
* setoid_rewrite t; [tac]Gravatar sacerdot2005-02-02
| | | | | | | | | | | 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
* Ajout cas VernacBackToGravatar herbelin2005-01-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6641 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
| | | | | | | | | 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
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
| | | | | | | "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
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
| | | | | | | | | | | | | | | | | * "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
* HUGE COMMITGravatar sacerdot2005-01-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant ↵Gravatar herbelin2005-01-02
| | | | | | dans redexpr.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6544 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵Gravatar herbelin2005-01-01
| | | | | | Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6541 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug transformation assert dans commit précédentGravatar herbelin2004-12-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6522 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)Gravatar herbelin2004-12-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise ↵Gravatar herbelin2004-12-27
| | | | | | 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
* Passage d'une bibliothèque de grands entiers naturels vers une ↵Gravatar herbelin2004-12-24
| | | | | | 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
* Hugo fixed a bug of refine, and it revealed a bug of functionalGravatar coq2004-12-10
| | | | | | | | 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
* Restauration type casted_open_constr pour tactique refine car l'unification ↵Gravatar herbelin2004-12-09
| | | | | | 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
* travail sur les types extraitsGravatar letouzey2004-12-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6441 85f007b7-540e-0410-9357-904b9bb8a0f7
* * added subst_evaluable_referenceGravatar sacerdot2004-12-07
| | | | | | | | * 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
* Code mortGravatar herbelin2004-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6420 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des ↵Gravatar herbelin2004-12-06
| | | | | | 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
* Orthographe!Gravatar herbelin2004-12-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction 1.138 appliquée à tort à la branche principale au lieu de ↵Gravatar herbelin2004-11-29
| | | | | | V8-0bugfix; retour version 1.137 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Commit précédent erroné; retour version précédenteGravatar herbelin2004-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6377 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ vis à vis de extratacticsGravatar herbelin2004-11-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6368 85f007b7-540e-0410-9357-904b9bb8a0f7
* When a reference to a constructor is met its inductive type must be closed.Gravatar sacerdot2004-11-18
| | | | | | | 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
* Locate ModuleGravatar herbelin2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6325 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command "Print Rewrite HindDb dbname".Gravatar sacerdot2004-11-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-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
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
| | | | | | | | | | | | | | | MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement dans les boxed values .Gravatar gregoire2004-11-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
* 'match term' now evaluates by default. Added 'lazy' keyword to delay the ↵Gravatar herbelin2004-10-11
| | | | | | evaluation of tactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6199 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression IsConjecture redondant avec ConjecturalGravatar herbelin2004-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6198 85f007b7-540e-0410-9357-904b9bb8a0f7
* un paquet de corrections de bugsGravatar letouzey2004-10-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6175 85f007b7-540e-0410-9357-904b9bb8a0f7
* The "Add Setoid" command now has a new argument "as name" that is usedGravatar sacerdot2004-10-01
| | | | | | | | | | to generate the name of the morphism. Previously the name was automatically generated, but this behaviour was not compatible with module typing: it was not possible to generate the same identifier in the module type and in the module. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
* cutrewrite does not work with relations that are not Coq-like equalities.Gravatar sacerdot2004-09-30
| | | | | | | | | | | | Thus it does not work for setoid relations and it can replace setoid_replace when the user wants to specify what the relation should be. To solve the problem this commit enables the syntax setoid_replace E1 with E2 using relation R ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
* New syntaxGravatar sacerdot2004-09-29
| | | | | | | | | | | "setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
* firstorder bugfix to cope with elim of sigma types with goal is of the wrong ↵Gravatar corbinea2004-09-27
| | | | | | sort git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6141 85f007b7-540e-0410-9357-904b9bb8a0f7
* restructuration des printers: proofs passe avant parsingGravatar barras2004-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_defsGravatar barras2004-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_defsGravatar barras2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de or-pattern pour le match-with v8Gravatar herbelin2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
* The innersort is now computed as the more precise sort between theGravatar sacerdot2004-09-08
| | | | | | | | | | | | | | synthesized innersort and the expected innersort. This closes a bug that allowed to export non well-typed* terms like the following one: ((fun (X : (T1 : CProp)) => (E : (T2 : Type))) : (T1 -> T2 : CProp)) * non well-typed according to the rules that consider CProp as a primitive sort. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6082 85f007b7-540e-0410-9357-904b9bb8a0f7
* The code used to compare the synthesized and the expected type (if available)Gravatar sacerdot2004-09-08
| | | | | | | | | | | | | | | | | | | | to decide whether a conversion should be generated (exporting both types). The comparison function used is Coq alpha conversion, that is also up to Casts. When it was successful, the only type that was kept was the synthesized one. In several CoRN theorems it happened that the expected type carried a few casts to make subterms of it be of type/sort CProp (instead of Type). These casts were forgot, and the innersort computed was imprecise. This partial fix consists in keeping the expected type. However, it may happen (at least in theory) that the casts to CProp are part of the synthesized type and not of the expected type. In this case they will be lost anyway. Properly fixing the problem would mean recur over the two alpha-convertible terms to add the casts from both sources. However, this operation is very expensive and I would prefer to avoid it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6081 85f007b7-540e-0410-9357-904b9bb8a0f7
* deuxieme vague de modifs: evar_defs fonctionnelGravatar barras2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
* reparation des Extract Constant avec HaskellGravatar letouzey2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ported to the new implementation of setoid_*.Gravatar sacerdot2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
* The old implementation of (setoid_replace c1 with c2) used to replaceGravatar sacerdot2004-09-03
| | | | | | | | | | either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation will not do it. Thus I am replacing every occurrence of (setoid_replace c1 with c2) with (setoid_replace c1 with c2 || setoid_replace c2 with c1). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6047 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 22:00:50 +0000