aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-09-30cutrewrite does not work with relations that are not Coq-like equalities.sacerdot
Thus it does not work for setoid relations and it can replace setoid_replace when the user wants to specify what the relation should be. To solve the problem this commit enables the syntax setoid_replace E1 with E2 using relation R ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6163 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-30setoid_replace E1 with E2sacerdot
now replaces E1 with E2 either generating the goal E1 R E2 or the goal E2 R E1 (as expected). Note: the relation R is guessed when more than one is applicable. This is not very nice, since it can guess the wrong one. Since making the tactic compute R requires much code refactoring, I would suggest the user to always use cutrewrite in place of setoid_rewrite. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6162 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6161 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29* error messages improvedsacerdot
* msg_warning no longer used (since it pretty prints the messages on the stderr and coqide does not show them). Is this a Coq bug??? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6160 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29Add Relation is now able to detect non well typed relation registrations.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6159 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The Add Morphism command is now able to detect in advance:sacerdot
1) if the proposed morphism named has already been used 2) if the proposed signature matches the function type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6158 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29New syntaxsacerdot
"setoid_rewrite dir term generate side conditions constr_list" to specify a list of side conditions that must be a subset of the generated new goals. Used to disambiguate in case of multiple set of generated side conditions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6157 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-29The Prod special case works only when the premise is of type Prop.sacerdot
This is now checked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6156 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 14:28:59 +0000