aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Ensures that let-in's in arities of inductive types work well. Maybe notGravatar herbelin2009-08-11
| | | | | | | | | very useful in practice but as soon as let-in's were not forbidden in the internal data structure, better to do it. Moreover, this gets closer to the view were inductive definitions are uniformly built from "contexts". (checker not changed!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12273 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout des .annot dans le .gitignore.Gravatar aspiwack2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12272 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed extra space in printing notation { x & P } + minor other thingsGravatar herbelin2009-08-11
| | | | | | (shorter proof of O_S in trunk + typo). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12271 85f007b7-540e-0410-9357-904b9bb8a0f7
* Infix (r12268 continued)Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12270 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add support for "Infix ... := constr" instead of just "Infix ... := ref".Gravatar herbelin2009-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12269 85f007b7-540e-0410-9357-904b9bb8a0f7
* Relatively ad hoc fix to an ill-typed instantiation bug in typeGravatar herbelin2009-08-11
| | | | | | | | | | | inference (see file failure/evar1.v) + fix of some CUMUL problems that were in the wrong direction. We assume for the fix that ill-typed unification problems come from subtyping where we don't know yet if a coercion has to be inserted or not, and hence are of the CUMUL form. More on suspending problems of the form ?n <= Type or Prop <= ?n has to be done yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12268 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
| | | | | | | | | 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
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12266 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
| | | | | | | | | | | | | | | (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
* Move out JMeq of subst for compatibility (it affects e.g. theGravatar herbelin2009-08-06
| | | | | | | | | 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
* changed deprecated setoid into relationGravatar amahboub2009-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12263 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
| | | | | | | | | | | | 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
* Fixed subst failing when a truly heterogeneous JMeq hyp is in theGravatar herbelin2009-08-04
| | | | | | | 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
* Added "etransitivity".Gravatar herbelin2009-08-03
| | | | | | | | | | | | 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
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
| | | | | | | | | | | | | | | - 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
* Fixed a typo in "info" for tactic "right".Gravatar herbelin2009-08-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12257 85f007b7-540e-0410-9357-904b9bb8a0f7
* csdpcert + unixGravatar fbesson2009-08-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12256 85f007b7-540e-0410-9357-904b9bb8a0f7
* addition of lia.cache - csdp.cache is now handled by micromega not csdpcertGravatar fbesson2009-07-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12255 85f007b7-540e-0410-9357-904b9bb8a0f7
* micromega : Better parsing of formulae - smaller proof terms for Z - ↵Gravatar fbesson2009-07-30
| | | | | | redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
* psatz Z -> psatz Z 1Gravatar fbesson2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
* Git ignore filesGravatar herbelin2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12252 85f007b7-540e-0410-9357-904b9bb8a0f7
* For git users, a global .gitignore fileGravatar letouzey2009-07-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12251 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArithGravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12250 85f007b7-540e-0410-9357-904b9bb8a0f7
* List: add a iff-based lemma about In and ++Gravatar letouzey2009-07-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12249 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"Gravatar letouzey2009-07-24
| | | | | | | 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
* Better comparison functions in OrderedTypeExGravatar letouzey2009-07-22
| | | | | | | | | | | | | | | 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
* Use unfold directly in unfold_equations. Fixes test-suite.Gravatar msozeau2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12246 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use camlp4 to accept some specific non-exhaustive patterns in groebnerGravatar letouzey2009-07-20
| | | | | | | | 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
* Move some examples for groebner into a test-suite fileGravatar letouzey2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12244 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in a commentGravatar letouzey2009-07-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12243 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Granted wish #2138 (support for local binders in syntax of Record fields).Gravatar herbelin2009-07-15
| | | | | | | | - 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
* - Fixing bug #2139 (kernel-based test of well-formation of eliminationGravatar herbelin2009-07-15
| | | | | | | | | | | | | | | | 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
* Simplify eauto and fix it for compatibility, allowing full delta duringGravatar msozeau2009-07-14
| | | | | | | unification for exact hints. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
| | | | | | | | | | | 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
* Allow coqdoc comments inside definition bodies.Gravatar msozeau2009-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 2134.Gravatar soubiran2009-07-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12235 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug #2116 ("simpl" created ill-typed term while acceptingGravatar herbelin2009-07-08
| | | | | | 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
* Don't use recent ocaml tolerance for pattern "ProjectVar _" whenGravatar herbelin2009-07-08
| | | | | | | 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
* Simplify addition of hints to a hint_db. Rebuild the dnet associatedGravatar msozeau2009-07-08
| | | | | | | | 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
* Use user-given implicits from the arity in inductive definitions.Gravatar msozeau2009-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12230 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reactivation of pattern unification of evars in apply unification, inGravatar herbelin2009-07-08
| | | | | | | | | | | | 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
* Add heuristic based on non-linearity of evars to determine whether anGravatar herbelin2009-07-08
| | | | | | | | 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
* Fixed anomaly when trying to load non existing file starting with "./" or "../".Gravatar herbelin2009-07-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12227 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug 2129 (evar introduced to remember an ambiguous projectionGravatar herbelin2009-07-08
| | | | | | | | | 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
* Completing support for F5=About by adding About to the state-preserving ↵Gravatar herbelin2009-07-08
| | | | | | command list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12225 85f007b7-540e-0410-9357-904b9bb8a0f7
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
| | | | | | | | | 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
* change in the order of unification constraints solving (for canonical ↵Gravatar amahboub2009-07-06
| | | | | | structures) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7
* repport of commit r12221Gravatar jforest2009-07-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12222 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12220 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new variants of [rewrite] and [autorewrite] which differ in theGravatar msozeau2009-06-30
| | | | | | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 00:00:35 +0000