aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* majGravatar filliatr2004-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6138 85f007b7-540e-0410-9357-904b9bb8a0f7
* no-assert en mode natifGravatar herbelin2004-09-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6137 85f007b7-540e-0410-9357-904b9bb8a0f7
* AjoutsGravatar herbelin2004-09-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6136 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ↵Gravatar herbelin2004-09-25
| | | | | | sub_match qui est renommé par ailleurs en match_subterm git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6133 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Prise en compte de Fail n (n>0) dans plusieurs cas qui avaientGravatar herbelin2004-09-25
| | | | | | | | | | | | | disparus dès la version 1.11 de proofs/tacinterp.ml - Prise en compte du contexte de filtrage sous-terme du but dans 'match goal with' quand des hypothèses aussi sont filtrées ce qui avait disparu dans la version 1.56 de proofs/tacinterp.ml - Restauration du filtrage sous-terme dans 'match c with' qui avait disparu dans la version 1.27 de tactics/tacinterp.ml - Nettoyage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6132 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6131 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6130 85f007b7-540e-0410-9357-904b9bb8a0f7
* New: (temporary) concrete syntax to specify the morphism signature:Gravatar sacerdot2004-09-24
| | | | | | | | | | | | | | "Add Morphism m @ arg1 ... argn @ out as ident" where argi = constr arrow and arrow = "-->" | "++>" | "==>" (for contravariant, covariant and bi-variant morphisms). The syntax should be improved by getting rid of the "@" and maybe choosing better symbols to represent the arrows. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout bug #255Gravatar herbelin2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifications concommitantes à la correction du bug #855Gravatar herbelin2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug report #855Gravatar herbelin2004-09-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6125 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6123 85f007b7-540e-0410-9357-904b9bb8a0f7
* error if binder was already definedGravatar barras2004-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6122 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6121 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6120 85f007b7-540e-0410-9357-904b9bb8a0f7
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-10 09:02:48 +0000