aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-09-291. major code clean-up for the Prod casesacerdot
2. cleaner behaviour: occurrences of the pattern in the type of a variable bound by a dependent product are no longer git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6155 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29impl is a reflexive relation (it used to be areflexive).sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6154 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29impl relation and impl/and/or/not morphisms over impl declared.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6153 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-291) bug fixed: new goals where compared according to the relation argumentssacerdot
only. Now the head of the relation is used to. 2) much nicer pretty-printing of the multiple set of side conditions that the tactic can now produce git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6152 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The list of possible solutions proposed by the tactic cannot contain anysacerdot
longer two set of goals such that the first is a subset of the second. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6151 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29Test updated.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6150 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29Hugly temporary notationsacerdot
Add Morphism constr @ arugments_list @ output as name replaced with the nicer (stable?) notation Add Morphism constr with signature signature as name git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6149 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The quoting function is now 100% complete.sacerdot
[ Note: untested, since the source of uncompleteness fixed is extremely unlikely to happen and it never happens in my test cases. ] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6148 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6147 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6146 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-28The quoting function is now almost complete (in the sense that it can findsacerdot
multiple solutions). Since several solutions are observationally equal (i.e. they open the same new set of goals), they are identified by the tactic. In case of multiple non observationally equal solutions, the list of them is presented to the user and the first one is randomically chosen. The user should be given a possibility to choose. Still todo: making the quoting function completely complete. Note: the wf_unifty_to_subterm is now called twice. The first time is not modulus delta conversion (the reasonable choice). The second time is modulus delta conversion and the call is made iff the first call failed. This is required by Ring that exploits the delta conversion ;-( git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6145 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6144 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27The quoting function of the reflexive tactic is now sound: all the termssacerdot
that it generates are well-typed Coq terms. A limited form of backtracking is used to avoid non well-typed choices. The function is not complete yet (since the backtracking algorithm is incomplete). This will be fixed shortly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6143 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27?(mod_delta=true) parameter added to each unification function.sacerdot
mod_delta = true if the unification is done modulus delta conversion (of closed terms). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6142 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27firstorder bugfix to cope with elim of sigma types with goal is of the wrong ↵corbinea
sort git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6141 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27corrected bug when lhs is matched w.r.t deltabarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6140 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-27collapse apps of patterns to avoid failuresbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6139 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6138 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-26no-assert en mode natifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6137 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-25Ajoutsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6136 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-25Remplacement de l'exception NextOccurrence _ par PatternMatchingFailure dans ↵herbelin
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
2004-09-25- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaientherbelin
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
2004-09-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6131 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6130 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24New: (temporary) concrete syntax to specify the morphism signature:sacerdot
"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
2004-09-24Ajout bug #255herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6127 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24Simplifications concommitantes à la correction du bug #855herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6126 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-24Correction bug report #855herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6125 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-23majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6123 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-23error if binder was already definedbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6122 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6121 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-22majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6120 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-22link order againbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6119 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-21majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6118 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-20majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6117 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-20pbs with link order and depsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6116 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-19majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6115 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6114 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17repaired depsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6112 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-16majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6111 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6110 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15put empty_env in hint clause (vo were becoming huge!)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6108 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6107 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-14majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6106 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-14evar tactic bugfixcorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6105 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-13majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6104 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-13* The ML tactic is now also aware of rewriting directions.sacerdot
* 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
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-08 21:45:39 +0000