aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* link order againGravatar barras2004-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6119 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6118 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6117 85f007b7-540e-0410-9357-904b9bb8a0f7
* pbs with link order and depsGravatar barras2004-09-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6116 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6115 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6114 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
* repaired depsGravatar barras2004-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6112 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6111 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6110 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
* put empty_env in hint clause (vo were becoming huge!)Gravatar barras2004-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6108 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6107 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6106 85f007b7-540e-0410-9357-904b9bb8a0f7
* evar tactic bugfixGravatar corbinea2004-09-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6105 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6104 85f007b7-540e-0410-9357-904b9bb8a0f7
* * The ML tactic is now also aware of rewriting directions.Gravatar sacerdot2004-09-13
| | | | | | | | | | | | * Code clean-up. * Preparation for the last implementation phase. The last implementation phase will consist in the algorithm that, performing backtracking, chooses the right combination of morphisms in the syntactic representation of the goal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6103 85f007b7-540e-0410-9357-904b9bb8a0f7
* The ML part of the tactic now knows about covariant and contravariant morphismGravatar sacerdot2004-09-13
| | | | | | | 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
* majGravatar filliatr2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6101 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6100 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
* majGravatar filliatr2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6098 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6097 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification de clenvGravatar barras2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code removed.Gravatar sacerdot2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6095 85f007b7-540e-0410-9357-904b9bb8a0f7
* 1. add_new_morphism now has a new optional argument that is the signatureGravatar sacerdot2004-09-10
| | | | | | | | | | 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
* add_new_morphism has now a new argument that is the signatureGravatar sacerdot2004-09-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add_new_morphism has now a new optional argument that is the signature ofGravatar sacerdot2004-09-10
| | | | | | | the morphism. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6092 85f007b7-540e-0410-9357-904b9bb8a0f7
* When refining a given term, the primitive refiner used to accepts some casts,Gravatar sacerdot2004-09-10
| | | | | | | | 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
* majGravatar filliatr2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6090 85f007b7-540e-0410-9357-904b9bb8a0f7
* CréditGravatar herbelin2004-09-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6089 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
* majGravatar filliatr2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6087 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6086 85f007b7-540e-0410-9357-904b9bb8a0f7
* unification encore...Gravatar barras2004-09-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6085 85f007b7-540e-0410-9357-904b9bb8a0f7
* * 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-27 12:59:49 +0000