aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* * cleaning/renaming in Setoids.vGravatar sacerdot2004-09-08
| | | | | | | * the data type for relations has been extended to cover all the cases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6084 85f007b7-540e-0410-9357-904b9bb8a0f7
* * cleaning/renamingGravatar sacerdot2004-09-08
| | | | | | | * reuse of definitions already given in the standard library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6083 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
* The Coq part of the reflexive part can now deal with irreflexive relations too.Gravatar sacerdot2004-09-08
| | | | | | | | | | | In particular it can deal with partial setoids (also called typoids). The latter feature was request by Marco Maggesi. This commit is just a porting of the ML part of the tactic to the new Coq part. It does not allow to exploit the new potentialities, yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6080 85f007b7-540e-0410-9357-904b9bb8a0f7
* The Coq part of the reflexive tactic is now able to handle alsoGravatar sacerdot2004-09-08
| | | | | | | | | | | irreflexive relations (in particular partial setoids, also called typoids). This feature was asked by Marco Maggesi. The Coq part of the tactic has now reached the planned expressive power. However, the ML part does not exploit yet the full expressiveness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6079 85f007b7-540e-0410-9357-904b9bb8a0f7
* petit bug avec les effets de bordsGravatar barras2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
* Meilleur anglais (cf #841)Gravatar herbelin2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6076 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵Gravatar herbelin2004-09-08
| | | | | | incorrects: 0 au lieu de 1 et lv dans le mauvait sens) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6075 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6073 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6072 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
* * The Coq part of the reflexive tactic setoid_rewrite is generalized toGravatar sacerdot2004-09-07
| | | | | | | | | | | asymmetric relations thanks to the introduction of morphisms that are covariant or contravariant in their arguments. * The ML part of the tactic is updated only for backward compatibility: it is still not possible to benefit from the asymmetric relations and relative morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6070 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6069 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6068 85f007b7-540e-0410-9357-904b9bb8a0f7
* mimick: unify types before making assignationGravatar barras2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6067 85f007b7-540e-0410-9357-904b9bb8a0f7
* optimized the non-backtracking caseGravatar barras2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6066 85f007b7-540e-0410-9357-904b9bb8a0f7
* bad env in mimick codeGravatar barras2004-09-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 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
* majGravatar filliatr2004-09-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6063 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction commit precedentGravatar herbelin2004-09-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6060 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6059 85f007b7-540e-0410-9357-904b9bb8a0f7
* deplacement de clenv vers pretypingGravatar barras2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 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
* Bug List.hd vs list_lastGravatar herbelin2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6056 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ options coqtop et coqcGravatar herbelin2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
* * New test (for setoid_replace in the general case)Gravatar sacerdot2004-09-03
| | | | | | | * Comments/to do changed (but still in italian) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6052 85f007b7-540e-0410-9357-904b9bb8a0f7
* * setoid_test.v removed and added again in new syntaxGravatar sacerdot2004-09-03
| | | | | | | * setoid_test.v8 ported to the new implementation of setoid_*. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6051 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
* New reflexive implementation of setoid_rewrite. The new implementationGravatar sacerdot2004-09-03
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | introduces a few backward incompatibilities: 1. setoid_replace used to try to close the new goal using full_trivial. The new implementation does not try to close the goal. To fix the script it is sufficient to add a "; [ idtac | trivial ]." after every application of setoid_replace that used to generate just one goal. 2. (setoid_replace c1 c2) used to replace either c1 with c2 or c2 with c1 (if c1 did not occur in the goal). The new implementation only replaces c1 with c2. To fix the script it is sufficient to replace (setoid_replace c1 with c2) with (setoid_replace c1 with c2) || (setoid_replace c2 with c1) in those cases where it is unknown what should be substituted with what. 3. the goal generated by the "Add Morphism" command has the hypothesis permutated w.r.t. the old implementation. I.e. the old implementation used to generate: forall x1 x2, forall x3 x4, x1=x2 -> x3=x4 -> ... whereas the new implementation generates forall x1 x2, x1=x2 -> forall x3 x4, x3 = x4 -> ... Fixing the script is usually trivial. 4. the "Add Morphism P" command used to generate a non-standard goal in the case of P being a predicate (i.e. a function whose codomain is Prop). In that case the goal ended with an implication (instead of ending with a coimplication). The new implementation generates a standard goal that ends with a coimplication. To fix the script you can add the following line at the very beginning: cut <<old_goal>>; intro Hold; split; apply Hold; assumption || (symmetry;assumption). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6049 85f007b7-540e-0410-9357-904b9bb8a0f7
* New command "Add Relation ..." (for the new implementation of setoid_*).Gravatar sacerdot2004-09-03
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 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
* V7 .v files for Setoid_* and Ring over setoids commented out.Gravatar sacerdot2004-09-03
| | | | | | | | | | To re-enable them I would need to back-port theories/Setoids/Setoid.v from the new syntax to the old syntax. However, since the translator is going to be removed from the next major Coq version, I am not doing it (unless required to). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6046 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6045 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6044 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6043 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6042 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6041 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6040 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6039 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dépendance en pa_ifdef dans la ligne camlp4deps de q_coqast induit make ↵Gravatar herbelin2004-08-26
| | | | | | depend en erreur; déplacement de pa_ifdef dans MMakefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6037 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6036 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1Gravatar herbelin2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Expansion du prédicat du 'match' vis à vis de la dépendance en le terme ↵Gravatar herbelin2004-08-24
| | | | | | filtré (utilisation de Anonymous pour signaler une dépendance formelle, en relation avec le nommage dans Inductiveops.type_case_branches); uniformisation/nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6032 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte expansion du prédicat du 'match' vis à vis de la ↵Gravatar herbelin2004-08-24
| | | | | | dépendance en le terme filtré (cf Indrec) + déplacement routines pour Cases à la V7 dans Pretyping) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)Gravatar herbelin2004-08-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Deplacement des fonctions de typage des predicate de Cases a la V7 de ↵Gravatar herbelin2004-08-24
| | | | | | inductiveops vers pretyping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6029 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-27 01:11:20 +0000