aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
in commit r12265. Add a few synonyms back in Libnames/Nameops to maintain some minimal compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12267 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
(uniformisation of function names, classification). One of the most visible change is the renaming of section_path into full_path (the use of name section was obsolete due to the module system, but I don't know if the new name is the best chosen one - especially it remains some "sp" here and there). - Simplification of the interface of classify_object (first argument dropped). - Simplification of the code for vernac keyword "End". - Other small cleaning or dead code removal. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-06Move out JMeq of subst for compatibility (it affects e.g. theherbelin
compilation of Grenoble/ATBR). Add subst' for subst extended with JMeq (maybe an option would be better??). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12264 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-05changed deprecated setoid into relationamahboub
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12263 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04- Add more precise error localisation when one of the application failsherbelin
in a chain of apply or apply-in. - Improved comments on the notions of permutation used in the library (still the equality relation in file Permutation.v misses the property of being effectively an equivalence relation, hence missing expected properties of this notion of permutation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12261 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-04Fixed subst failing when a truly heterogeneous JMeq hyp is in theherbelin
context (problem introduced in r12259) + improved backward compatibility in hippatern.mli (wrt r12259). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12260 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-03Added "etransitivity".herbelin
Added support for "injection" and "discriminate" on JMeq. Seized the opportunity to update coqlib.ml and to rely more on it for finding the equality lemmas. Fixed typos in coqcompat.ml. Propagated symmetry convert_concl fix to transitivity (see 11521). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Improved parameterization of Coq:herbelin
- add coqtop option "-compat X.Y" so as to provide compatibility with previous versions of Coq (of course, this requires to take care of providing flags for controlling changes of behaviors!), - add support for option names made of an arbitrary length of words (instead of one, two or three words only), - add options for recovering 8.2 behavior for discriminate, tauto, evar unification ("Set Tactic Evars Pattern Unification", "Set Discriminate Introduction", "Set Intuition Iff Unfolding"). Update of .gitignore git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-02Fixed a typo in "info" for tactic "right".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12257 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-08-01csdpcert + unixfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-31addition of lia.cache - csdp.cache is now handled by micromega not csdpcertfbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30micromega : Better parsing of formulae - smaller proof terms for Z - ↵fbesson
redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30psatz Z -> psatz Z 1fbesson
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30Git ignore filesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12252 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-30For git users, a global .gitignore fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12251 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24List: add a iff-based lemma about In and ++letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-24Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"letouzey
I wonder how many of us were aware of the existence of such syntax ;-) Anyway, it is now subsumed by "rewrite by". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12248 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-22Better comparison functions in OrderedTypeExletouzey
The compare functions are still functions-by-tactics, but now their computational parts are completely pure (no use of lt_eq_lt_dec in nat_compare anymore), while their proofs parts are simply calls to (opaque) lemmas. This seem to improve the efficiency of sets/maps, as mentionned by T. Braibant, D. Pous and S. Lescuyer. The earlier version of nat_compare is now called nat_compare_alt, there is a proof of equivalence named nat_compare_equiv. By the way, various improvements of proofs, in particular in Pnat. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12247 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use unfold directly in unfold_equations. Fixes test-suite.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12246 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Use camlp4 to accept some specific non-exhaustive patterns in groebnerletouzey
The camlp4 extension "refutpat" provides a syntax let* for pattern that are non-exhaustive on purpose (e.g. let* x::l = foo in ...). A Failure is raised if the pattern doesn't match the expression. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12245 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Move some examples for groebner into a test-suite fileletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-20Typo in a commentletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12243 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-15- Granted wish #2138 (support for local binders in syntax of Record fields).herbelin
- Add tests related to commits 12229 (bug #2117) and 12241 (bug #2139). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12242 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-15- Fixing bug #2139 (kernel-based test of well-formation of eliminationherbelin
predicate called from proof refiner was failing because it was not aware of evars instantiation; I added a nf_evar in 8.2 branch but for the trunk, I propose to remove the elimination predicate well-formation test; we therefore assume that tactics build correct elimination predicates in Case, is it not too much demanding?). - Seized the opportunity to remove dead kernel code about non dependent elimination predicates (all predicates are stored dependent by default since a few years now). - Anecdotic complement to commit 12229 (removal of obsolete comment). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12241 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-14Simplify eauto and fix it for compatibility, allowing full delta duringmsozeau
unification for exact hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12239 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Use the proper unification flags in e_exact. This makes exact fail a bitmsozeau
more often but respects the spec better. The changes in the stdlib are reduced to adding a few explicit [unfold]s in FMapFacts (exact was doing conversion with delta on open terms in that case). Also fix a minor bug in typeclasses not seeing typeclass evars when their type was a (defined) evar itself. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12238 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Allow coqdoc comments inside definition bodies.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-09Correction bug 2134.soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12235 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Fixed bug #2116 ("simpl" created ill-typed term while acceptingherbelin
inverting a recursive constant with dependent K-parameters). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12233 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Don't use recent ocaml tolerance for pattern "ProjectVar _" whenherbelin
ProjectVar is a constant constructor (anyway, use of _ for constant constructor was here by mistake). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12232 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Simplify addition of hints to a hint_db. Rebuild the dnet associatedmsozeau
with it when the transparent state changes and not only when [Hint Unfold] is added. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12231 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Use user-given implicits from the arity in inductive definitions.msozeau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12230 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Reactivation of pattern unification of evars in apply unification, inherbelin
agreement with wish #2117 (pattern unification of evars remained deactivated for 3 years because of incompatibilities with eauto [see commit 9234]; thanks to unification flags, it can be activated for apply w/o changing eauto). Also add test for bug #2123 (see commit 12228). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12229 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Add heuristic based on non-linearity of evars to determine whether anherbelin
evar is dependent or not (solve bug #2123). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12228 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Fixed anomaly when trying to load non existing file starting with "./" or "../".herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Fixing bug 2129 (evar introduced to remember an ambiguous projectionherbelin
had wrong type). At least two problems remain: - projection involving evar should check the type are compatible, - instances of filtered evars should not be shrinked as all values are needed to ensure the well-typedness of the instanciated restricted evars. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12226 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-08Completing support for F5=About by adding About to the state-preserving ↵herbelin
command list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-07Jolification : tentative de supprimer les "( evd)" et associés quiaspiwack
traînaient un peu partout dans le code depuis la fusion d'evar_map et evar_defs. Début du travail d'uniformisation des noms donnés aux evar_defs à travers le code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12224 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-06change in the order of unification constraints solving (for canonical ↵amahboub
structures) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-04repport of commit r12221jforest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-07-01Support for binding Coq root read-only in -R optionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-30Add new variants of [rewrite] and [autorewrite] which differ in themsozeau
selection of occurrences. We use a new function [unify_to_subterm_all] to return all occurrences of a lemma and produce the rewrite depending on a new [conditions] option that controls if we must rewrite one or all occurrences and if the side conditions should be solved or not for a single rewrite to be successful. [rewrite*] will rewrite the first occurrence whose side-conditions are solved while [autorewrite*] will rewrite all occurrences whose side-conditions are solved. Not supported by [setoid_rewrite] yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12218 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-29Miscellaneous practical commits: herbelin
- theories: made a hint database with the constructor of eq_true - coqide: binding F5 to About dans coqide + made coqide aware of string interpretation inside comments - lexer: added warning when ending comments inside a strings itself in a comment - xlate: completed patten-matching on IntroForthComing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-29Fix bug introduced by last revision, subtac_cases was returning themsozeau
wrong tycon. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12216 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-28Raise an error and not an anomaly if a rewrite is attempted on amsozeau
dependent argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12215 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-28Abstract the tycon by the matched terms when turning them into variablesmsozeau
in Program's pattern-matching compilation (fixes bug #2131). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12214 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-28Improve return predicate inference by making the return type dependentmsozeau
on a matched variable when it is of dependent type, when its type allows it (no constructor in the real arguments). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12213 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-06-26propagation sur le trunk du commit 12101 soubiran
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12212 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-21 00:23:13 +0000