aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-06-25bug 2328 fixed: failure when polynomial not i idealpottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13195 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25modifs de nsatz suggerees par Hugopottier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13194 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-25Restored a "feature" of unification in pre-8.3 (it was used e.g. in aherbelin
proof of Chung-Kil's Hur Heq package): conversion in "trivial_unify" accepted evars as ordinary variables. I hope I did not invalidate some features that would have needed restricting conversion on evar-free terms, but since failure of conversion in presence of evars is redirected to the main unification algorithm, I guess it is OK. For better readibility, I also inlined and cleaned a bit trivial_unify. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13193 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Extraction: nicer simple extraction of custom defs (fix #2204)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13192 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Names: remove obsolete mod_self_idletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13190 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Ajout d'une feuille de style pour les définitions spécifiques à Hevea + ↵notin
divers corrections sur la génération du manuel de référence. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13186 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-23Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ↵notin
coq.inria.fr) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13185 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Commit 13179 continued (updated CHANGES about support for Heq's library).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13181 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Backport from trunk to 8.3 of modifications on groebner/nsatzherbelin
(13056-13058, 13062, 13069, 13073). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13180 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Added Chung-Kil Hur's smart "pattern" tactic (h_resolve).herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13179 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Fixing dependencies for coqidevgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13178 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22fix bug #2318, parsing error on dos line endingsvgross
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13177 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
Applied it to fix mli file headers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-06-21Extraction: replace unicode characters in ident by ascii encodings (fix ↵letouzey
#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
2010-06-20Test script for bug #1962 (that is apparently solved in 8.3+trunk :-)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13172 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:28:08 +0000