aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Protection against anomaly when loading a state with bad magic number.Gravatar herbelin2010-06-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: replace unicode characters in ident by ascii encodings (fix ↵Gravatar letouzey2010-06-21
| | | | | | | | | | | | | | | | | | | #2158,#2179) Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is the hexa code for the unicode index of this character. For instance <alpha> is turned into __U03b1_. I know, this is ugly. Better solutions are welcome, but I'm afraid we can't do much better as long as ocaml and haskell don't accept unicode letters in idents. At least, this way we're pretty sure this translating won't create name conflit, as long as extraction users avoid __ in their names, something that they should already do btw (see for instance extraction of coinductive types in ocaml). Yes, I should add a test and a warning/error in case of use of __ someday. NB: this commit belongs proudly to the quick'n'dirty category git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7
* Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)Gravatar letouzey2010-06-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
* clear/revert dependent: restrict to hyp(h) instead of ident(h)Gravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13169 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13168 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hack for fixing bug #2172 (see explanations in file rewrite-2172.v).Gravatar herbelin2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13167 85f007b7-540e-0410-9357-904b9bb8a0f7
* Documentation of clear dependent and revert dependentGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13166 85f007b7-540e-0410-9357-904b9bb8a0f7
* add in test-suite the scripts about fsetdec bugsGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13165 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report fixes from FSetDecide to MSetDecideGravatar letouzey2010-06-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13164 85f007b7-540e-0410-9357-904b9bb8a0f7
* fsetdec: a forgotten Set instead of Type was breaking discard_nonFset (fix ↵Gravatar letouzey2010-06-18
| | | | | | #2281) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13163 85f007b7-540e-0410-9357-904b9bb8a0f7
* fsetdec: clear dependent hypothesis before anything else (fix #2136).Gravatar letouzey2010-06-17
| | | | | | | | | 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
* New tactic "clear dependent", for the moment in ltac in Init/TacticsGravatar letouzey2010-06-17
| | | | | | | | | | | 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
* test for bug #2141 (include + extraction)Gravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13160 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetInterface: no induction principle about a Record (nicer extraction)Gravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13159 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: fix the eta reduction function used in code optimisationsGravatar letouzey2010-06-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13158 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSetAVL: for nicer extraction, we create only tree_ind, not tree_rect and ↵Gravatar letouzey2010-06-15
| | | | | | tree_case git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13156 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGE: a word about new commands Compute and FailGravatar letouzey2010-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13155 85f007b7-540e-0410-9357-904b9bb8a0f7
* CHANGES: list of modifications for the extractionGravatar letouzey2010-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13138 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction: in support library, more and nicer big_intGravatar letouzey2010-06-15
| | | | | | | | | - 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
* Update of Extraction documentationGravatar letouzey2010-06-14
| | | | | | | | | | | | - 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
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
| | | | | | | | | | 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
* Alert on the possible incompatibilties with set_add (see bug 2111) whichGravatar herbelin2010-06-14
| | | | | | 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
* Extraction Implicit: documentationGravatar letouzey2010-06-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13133 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added printing of recursive notations in cases pattern (supported by wish 2248).Gravatar herbelin2010-06-14
| | | | | | | 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
* Fixing bug 2295 (omission of option "as" in return clause of "match" was notGravatar herbelin2010-06-13
| | | | | | working with section/goal variables). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13131 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2300 (ltac pattern-matching returning terms with concrete universes).Gravatar herbelin2010-06-13
| | | | | | | | 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
* Addressed bug #2320 in v8.2 and v8.3 branches ("refine" problem withGravatar herbelin2010-06-13
| | | | | | | | 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
* Fixing definition of set_map (bug report #2111) which was actually alreadyGravatar herbelin2010-06-13
| | | | | | 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
* Addressed bug #2310 and replaced anomaly "unknown meta" raised by "refine"Gravatar herbelin2010-06-13
| | | | | | | | | | | | 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
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
| | | | | | enough) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13126 85f007b7-540e-0410-9357-904b9bb8a0f7
* Made intros_until and onInductionArg a bit stricter and robustGravatar herbelin2010-06-13
| | | | | | | | | | | | | 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
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
| | | | | | | 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
* Fixed bug #2135 (second-order unification was raising cryptic message)Gravatar herbelin2010-06-12
| | | | | | | | | | | - 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
* Added regression tests for bugs + miscellaneous improvementsGravatar herbelin2010-06-12
| | | | | | | | | - #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
* Applying François' patch fixing grammar of uniform inheritance condition ↵Gravatar herbelin2010-06-12
| | | | | | | | message (see bug report #2331) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13120 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved the inference of the return predicate in dependent pattern-matching.Gravatar herbelin2010-06-12
| | | | | | | | | | | | | | 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
* Added rudimentary support for using constructors from the explicitGravatar herbelin2010-06-12
| | | | | | | | 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
* Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).Gravatar herbelin2010-06-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13116 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added debugging printer for the idmap used at evar definition time forGravatar herbelin2010-06-12
| | | | | | 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
* Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.Gravatar herbelin2010-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13114 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).Gravatar herbelin2010-06-11
| | | | | | | | | | | | | | | | 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
* Fixed two bugs in pattern-matching compilationGravatar herbelin2010-06-10
| | | | | | | | | | | | | | | | - 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
* Fixed a very old (from V6.3) typo in headers.styGravatar herbelin2010-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Extraction Implicits: can accept argument names instead of just positionsGravatar letouzey2010-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13109 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix build with OCaml 3.12Gravatar glondu2010-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13107 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug # 2303 in r 13087.Gravatar msozeau2010-06-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tentative fix for bug #2226: put inj_pair2 and eq_dep_eq hints in aGravatar msozeau2010-06-09
| | | | | | | different (eqdep) database. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
| | | | | | | | | | 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
* Fix bug #2262: bad implicit argument number by avoiding countingGravatar msozeau2010-06-09
| | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-22 22:39:11 +0000