aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-06-18clear/revert dependent: restrict to hyp(h) instead of ident(h)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13168 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Documentation of clear dependent and revert dependentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13166 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18add in test-suite the scripts about fsetdec bugsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18Report fixes from FSetDecide to MSetDecideletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13164 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-18fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix ↵letouzey
#2281) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13163 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-17fsetdec: clear dependent hypothesis before anything else (fix #2136).letouzey
Since the tactic fsetdec is doing lots of "clear" and also "subst" on equalities, things may go wrong in case of dependencies amongst hypothesis. For the moment, we clear all hypothesis that mention other hypothesis of sort Prop. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13162 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-17New tactic "clear dependent", for the moment in ltac in Init/Tacticsletouzey
for the moment, only one hypothesis name is accepted after clear dependent (seems to be also the case for generalize dependent). Btw, added an alternative name "revert dependent" for "generalize dependent", since this tactics remove hypothesis from the context. To be documentated later... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13161 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-16test for bug #2141 (include + extraction)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13160 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-16MSetInterface: no induction principle about a Record (nicer extraction)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13159 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-16Extraction: fix the eta reduction function used in code optimisationsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13158 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-15MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and ↵letouzey
tree_case git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13156 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-15CHANGE: a word about new commands Compute and Failletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13155 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-15CHANGES: list of modifications for the extractionletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13138 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-15Extraction: in support library, more and nicer big_intletouzey
- we use a wrapper file big.ml to have short names about big_int and specialized functions for extraction - new files : ExtrOcamlZInt for Z==>int and N==>int, ExtrOcamlZBigInt for Z==>big_int and N==>big_int git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13137 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Update of Extraction documentationletouzey
- Removal of the notice about the "experimental" status of extraction. Of course extraction is still experimental, but no less than the rest of Coq ;-) - Removal of the example about heapsort now that Heap is obsolete. - Euclid isn't the best of the examples, but for the moment we leave it - We mention ExtrOcamlIntConv and the others extraction/*.v - Various small improvements git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13136 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Fixed commit 13125 (stricter check of induction args): an interpretationherbelin
checking function was used instead of a test of existence in the context. Also restricted constr_of_id which had no reason to interpret a posteriori an already interpreted identifier as a global reference. Consequently adapted funind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13135 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Alert on the possible incompatibilties with set_add (see bug 2111) whichherbelin
was actually used in the contribs (MiniC). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13134 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Extraction Implicit: documentationletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13133 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-14Added printing of recursive notations in cases pattern (supported by wish 2248).herbelin
Note that the code is no longer in constrextern.ml but in topconstr.ml where the code for reversing notations of term already was. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2295 (omission of option "as" in return clause of "match" was notherbelin
working with section/goal variables). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13131 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).herbelin
By the way, there is an open problem of which conversion to use (conv, evarconv, with or w/o universes levels) when trying to unify multiple instances of the same variable in ltac pattern-matching. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13130 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withherbelin
metas in return predicate of "match"); propagated protection for #2310 ("refine" problem with dependent metas of higher-order type) in v8.3 to v8.2. Everything goes well in trunk thanks for the new proof engine. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13129 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixing definition of set_map (bug report #2111) which was actually alreadyherbelin
incorrect when it was introduced in 1998. Proofs about it remain to be done... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13128 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"herbelin
by a regular error in v8.3. Example behaves better in trunk thanks to new proof engine. In fact, there are two distinct solutions to a unification problem: should "refine" commit to one of them or leave the problem open? For trunk, improved the unification error message by enforcing nf_evar (but at some time, nf_evar in error messages should move to himsg because it is costly when errors are used for backtracking). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13127 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Made intros_until and onInductionArg a bit stricter and robustherbelin
The tolerance for overloading "id" as quantified hypothesis and as declared variable is kept - because induction_arg entry is not available to extended tactics, e.g. "discriminate", and these extensions do not know a priori if a name is quantified or declared. However, an upstream check is done to ensure that an induction argument exists as term if not quantified so that the tactics do not have to check this individually by themselves. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13125 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-13Fixed a bug in pretty-printing "induction" and "destruct" due to aherbelin
swap in the evar flags and the isrec flag. (e.g. "induction" was printed "edestruct"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13124 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed bug #2135 (second-order unification was raising cryptic message)herbelin
- made the example work (a call to whd_meta was missing) - replaced the internal error messages of w_unify_to_subterm_list into user-understandable messages - incidentally fixed the meaning of whd_meta (which now takes an evd) and meta_name (which now does what it means and do not treat differently the instantiated metas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13122 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added regression tests for bugs + miscellaneous improvementsherbelin
- #2095 (not fixed in v8.2 but fixed in v8.3 and trunk) - #2108 (fixed in v8.2, v8.3, trunk) - #2102 (moved warning to msg_warning to ensure flushing, but still open enhancement) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13121 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Applying François' patch fixing grammar of uniform inheritance condition ↵herbelin
message (see bug report #2331) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13120 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Improved the inference of the return predicate in dependent pattern-matching.herbelin
More precisely, the mecanism used to automatically infer return predicates of the form "as x in I y1..yn match y1..yn x with u1(z1)..un(zn) => P(z1..zn) | _ => ID end" now computes the dependencies in the types of y1..yn and x. This allows it to benefit of the generalisation mechanism of the pattern-matching compilation algorithm ("Abstract") and to infer more sophisticated return predicates (e.g. when working with "vector"). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13118 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added rudimentary support for using constructors from the explicitherbelin
substitution of evars when solving equation "?n[subst] = t": this is a quite common useful heuristic for inferring the return predicate of "match". Made incidentally a minor simplification of expand_full_opt. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13117 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13116 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-12Added debugging printer for the idmap used at evar definition time forherbelin
compacting the explicit substitution of the evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13115 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-11Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13114 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
Use two ways to solve it: - added a whd_betaiota in solve_simple_eqn (since evarconv itself refuses beta to preserve the opportunities of first-order-matching expressions of the form "(fun x => P) t"; an advantage of this whd_betaiota is also that it may simplify K-redexes. - also added a last-chance test in case of failing occur-check by trying to fully head-normalize (with delta) the right-hand-side (allows to solve for instance "?n = id ?n" where id is a constant (a bridled form of solve_refl that use fconv instead of evar_conv_x). Incidentally improved a bit the rendering of the type of generalized terms in pattern-matching by using whd_betaiota. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13113 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Fixed two bugs in pattern-matching compilationherbelin
- first bug was a missing lift when the return predicate was assumed to be a simple evar - second problem was in the inference of a custom inversion predicate in case of matching on a term in a constrained type (like "vect (S n)"): the rel bound to local definitions in the instance of evars where instantiated (by other evars) which is wrong per se but which contradicted the assumptions of find_projectable_vars in evarutil.ml which assumed that this did not occur; solved the problem by not instantiating references to local definition which (probably) will not loose some opportunity of unification in presence of non unfolded local definitions, ... - also cleaned a bit prepare_predicate git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13112 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Fixed a very old (from V6.3) typo in headers.styherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13110 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Extraction Implicits: can accept argument names instead of just positionsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-10Fix build with OCaml 3.12glondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13107 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fixed bug # 2303 in r 13087.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13104 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in amsozeau
different (eqdep) database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13103 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2317: setoid_rewrite ignored binding lists. Slightlymsozeau
generalize the interface of Clenv to be able to use the existing treatment of bindings. Clenv functions did not use goals conclusions but insisted on getting goals anyway (which is even more problematic as goals appear in evar maps now). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13102 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Fix bug #2262: bad implicit argument number by avoiding countingmsozeau
products as implicit if they're part of a term and not a type (issue a warning instead). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13101 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Keep description of Automatic Introduction at only one place of CHANGES.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13100 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Relaxed the freshness constraint in "intro H" (with "H" explicit):herbelin
don't forbid to overwrite a global reference of same basename. Should hopefully be more convenient. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13099 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-09Allowing to use an ordering different than Lt with measurejforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13098 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-01 02:53:43 +0000