aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-09-13The ML part of the tactic now knows about covariant and contravariant morphismsacerdot
arguments. However, it still does not know about rewrite directions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6102 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6101 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-12majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6100 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-12inclusion de meta_map dans evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6099 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6098 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6097 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10simplification de clenvbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10Dead code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6095 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-101. add_new_morphism now has a new optional argument that is the signaturesacerdot
2. partial setoids (a.k.a. areflexive relations) are now properly supported 3. the first two arguments of proj2 in the proof term have been simplified to be just the mutual coimplication of the old and the new goal. 4. code simplification git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6094 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10add_new_morphism has now a new argument that is the signaturesacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6093 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10Add_new_morphism has now a new optional argument that is the signature ofsacerdot
the morphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6092 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-10When refining a given term, the primitive refiner used to accepts some casts,sacerdot
but to ignore others. This commit ensures that casts are always dealt properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6091 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6090 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Créditherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6089 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-09Ajout de or-pattern pour le match-with v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6088 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6087 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6086 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08unification encore...barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08* cleaning/renaming in Setoids.vsacerdot
* 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
2004-09-08* cleaning/renamingsacerdot
* 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
2004-09-08The innersort is now computed as the more precise sort between thesacerdot
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
2004-09-08The code used to compare the synthesized and the expected type (if available)sacerdot
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
2004-09-08The Coq part of the reflexive part can now deal with irreflexive relations too.sacerdot
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
2004-09-08The Coq part of the reflexive tactic is now able to handle alsosacerdot
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
2004-09-08petit bug avec les effets de bordsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6078 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08Meilleur anglais (cf #841)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6076 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-08Un bug de simpl de 1995 + nettoyage (les args de list_fold_left_i etaient ↵herbelin
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
2004-09-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6073 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6072 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07deuxieme vague de modifs: evar_defs fonctionnelbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-07* The Coq part of the reflexive tactic setoid_rewrite is generalized tosacerdot
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
2004-09-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6069 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6068 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06mimick: unify types before making assignationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6067 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06optimized the non-backtracking casebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6066 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06bad env in mimick codebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6065 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-06reparation des Extract Constant avec Haskellletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-05majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6063 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-04Correction commit precedentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6062 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6060 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6059 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03deplacement de clenv vers pretypingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Bug List.hd vs list_lastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6056 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJ options coqtop et coqcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03* New test (for setoid_replace in the general case)sacerdot
* 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
2004-09-03* setoid_test.v removed and added again in new syntaxsacerdot
* 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
2004-09-03Ported to the new implementation of setoid_*.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6050 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03New reflexive implementation of setoid_rewrite. The new implementationsacerdot
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
2004-09-03New command "Add Relation ..." (for the new implementation of setoid_*).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6048 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 22:23:35 +0000