aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
| | | | | | | | | | | - reinstall (x : T | P) binder syntax extension. - fix a wrong Evd.define in coercion code. - Simplify interface of eterm_obligations to take a single evar_map. - Fix a slightly subtle bug related to resolvability of evars: some were marked unresolvable and never set back to resolvable across calls to typeclass resolution. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hopefully complying with camlp5 < 6.00 syntaxGravatar herbelin2012-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15055 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2709: Duplication in coqdoc index entriesGravatar pboutill2012-03-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15053 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefMan: Environment variables description updateGravatar pboutill2012-03-19
| | | | | | There is no mention in the refman of relative search of the lib from the binaries directory and of the use of _CoqProject by CoqIdE. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes bug: #2692 (Arguments/simpl off by 1)Gravatar gareuselesinge2012-03-19
| | | | | | | simpl was accessing the reduction stack at position n when the length of the stack was exactly n. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15049 85f007b7-540e-0410-9357-904b9bb8a0f7
* Arguments/simpl: allow ! even on non fixpointsGravatar gareuselesinge2012-03-19
| | | | | | | | | | | | | | | It is now possible to tell simpl to unfold a constant that hides no "match" but is applied to concrete arguments. Arguments id _ !n. Goal forall x, id x = id 2. intros; simpl. x : nat ======== id x = 2 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Yet another subtlety with bug 2732: when several grammar rules of aGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | TACTIC EXTEND block possibly parse the stand-alone name of a tactic, then only the first rule must be registered in the atomic tactic table so as to be consistent with what happens when the tactic is invoked directly via its parsing rules and not via the interpretation of a reference in the atomic tactic table. Concretely, this affects TACTIC EXTEND blocks of the form TACTIC EXTEND foo [ "bar" tactic_opt(tac) -> ... ] | [ "bar" constr_list(tac) -> ... ] where both rules parses "bar" alone but only the first rule must be registered in the atomic table, git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15046 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removing redundant entry int_nelist and removing extra space whenGravatar herbelin2012-03-18
| | | | | | printing occurrences list. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15044 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing bug #2732 (anomaly when using the tolerance for writingGravatar herbelin2012-03-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | "f atomic_tac" as a short-hand for "f ltac:(atomic_tac)" for "f" an Ltac function - see Tacinterp.add_primitive_tactic). More precisely, when parsing "f ref" and "ref" is recognized as the name of some TACTIC-EXTEND-defined tactic parsable as an atomic tactic (like "eauto", "firstorder", "discriminate", ...), the code was correct only when a rule of the form `TACTIC EXTEND ... [ "foo" -> ...] END' was given (where "foo" has no arguments in the rule) but not when a rule of the form `TACTIC EXTEND ... [ "foo" tactic_opt(p) -> ...] END' was given (where "foo" had an optional argument in the rule). In particular, "firstorder" was in this case. More generally, if, for an extra argument able to parse the empty string, a rule `TACTIC EXTEND ... [ "foo" my_special_extra_arg(p) -> ...] END' was given, then "foo" was not recognized as parseable as an atomic string (this happened e.g. for "eauto"). This is now also fixed. There was also another bug when the internal name of tactic was not the same as the user-level name of the tactic. This is the reason why "congruence" was not recognized when given as argument of an ltac (its internal name is "cc"). Incidentally removed the redundant last line in the parsing rule for "firstorder". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15041 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge and add missing file.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15040 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix merge.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15039 85f007b7-540e-0410-9357-904b9bb8a0f7
* Revise API of understand_ltac to be parameterized by a flag for resolution ↵Gravatar msozeau2012-03-14
| | | | | | | | | of evars. Used when interpreting a constr in Ltac: resolution is now launched if the constr is casted. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge fixesGravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15037 85f007b7-540e-0410-9357-904b9bb8a0f7
* Final part of moving Program code inside the main code. Adapted ↵Gravatar msozeau2012-03-14
| | | | | | add_definition/fixpoint and parsing of the "Program" prefix. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15036 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integrated obligations/eterm and program well-founded fixpoint building to ↵Gravatar msozeau2012-03-14
| | | | | | | | toplevel/ The code is not called yet from there. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
* Everything compiles again.Gravatar msozeau2012-03-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Second step of integration of Program:Gravatar msozeau2012-03-14
| | | | | | | | - Remove useless functorization of Pretyping - Move Program coercion/cases code inside pretyping/, enabled according to a flag. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove support for "abstract typing constraints" that requires unicity of ↵Gravatar msozeau2012-03-14
| | | | | | | | | | | solutions to unification. Only allow bidirectional checking of constructor applications, enabled by a program_mode flag: it is backwards-incompatible due to delta-reduction, constructor parameters might get instantiated with delta-equivalent but not syntactically equivalent terms. Prepare for merging the Program-specific version of Pretyping/Cases/Coercion with the main code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15032 85f007b7-540e-0410-9357-904b9bb8a0f7
* A bit of cleaning: unifying push_rels and push_rel_context.Gravatar herbelin2012-03-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15031 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
| | | | | | | | did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: avoid recording dummy universe constraints u<=u or u=uGravatar letouzey2012-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15026 85f007b7-540e-0410-9357-904b9bb8a0f7
* Glob_term.predicate_pattern: No number of parameters with letins.Gravatar pboutill2012-03-02
| | | | | | | | | Detyping is wrong about it and as far as I understand no one but Constrextern uses it. Constrextern has now the same machinery for all patterns. Revert if I miss something. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15022 85f007b7-540e-0410-9357-904b9bb8a0f7
* "Let in" in pattern hell, one more iterationGravatar pboutill2012-03-02
| | | | | | | | This reverts commit 28bcf05dd876beea8697f6ee47ebf916a8b94cdf. An other wrong externalize function git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15021 85f007b7-540e-0410-9357-904b9bb8a0f7
* Noise for nothingGravatar pboutill2012-03-02
| | | | | | | | | | | Util only depends on Ocaml stdlib and Utf8 tables. Generic pretty printing and loc functions are in Pp. Generic errors are in Errors. + Training white-spaces, useless open, prlist copies random erasure. Too many "open Errors" on the contrary. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
| | | | | | | | | | | univ_depends checks whether a universe variable appears or is equal to a universe. In comparison with the previous hack in inductiveops based on try...catching UniverseInconsistency, this should be semantically equivalent, simplier, and more robust in case we allow someday an unsafe mode where merge_constraints would be a no-op. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15013 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: a better Constraint.compareGravatar letouzey2012-03-01
| | | | | | | Let's gain a few % by not using Pervasive.compare on a structure containing some universe_levels, but rather UniverseLevel.compare on them. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15012 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrects the erroneous error message when trying to unfocus a fullyGravatar aspiwack2012-03-01
| | | | | | unfocused proof (part of bug #2671). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15011 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed a superfluous function in proof.mli. Preparing for incomingGravatar aspiwack2012-03-01
| | | | | | changes of the handling of unfocusing errors. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15010 85f007b7-540e-0410-9357-904b9bb8a0f7
* New version of recdef :Gravatar jforest2012-03-01
| | | | | | | + Allowing much more function to be defined. + Using completely new algorithm to define non structural fixpoints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15009 85f007b7-540e-0410-9357-904b9bb8a0f7
* various corrections in invfun due to a modification in inductionGravatar jforest2012-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15008 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: a faster is_leq test used when possibleGravatar letouzey2012-02-29
| | | | | | | | | | | | Let's reintroduce the idea of stopping the graph traversal as soon as a LE arc has been found, but this time we do so only when we're not interested by the LT/LE distinction. This way, we should remain correct but avoid largly the time penalty induced by the last fix on univ.ml: the +30% on contrib Container is almost gone, let's hope it'll be the same with Ssreflect. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15007 85f007b7-540e-0410-9357-904b9bb8a0f7
* correcting a little bug in invfun.mlGravatar jforest2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15005 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction of bug 2457Gravatar jforest2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15004 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation of Constrintern...Gravatar pboutill2012-02-29
| | | | | | I love being push under presure to commit and do not try my fixup ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15003 85f007b7-540e-0410-9357-904b9bb8a0f7
* RefMan update about match syntax.Gravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15002 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the syntax of pattern matching, the arguments of the inductive in the "in"Gravatar pboutill2012-02-29
| | | | | | | | clause can be any pattern. It is expanded as a match in the return clause. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15001 85f007b7-540e-0410-9357-904b9bb8a0f7
* In the syntax of pattern matching, "in" clauses are patterns.Gravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15000 85f007b7-540e-0410-9357-904b9bb8a0f7
* Vector: missing injection lemmas and better impossible branchesGravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14999 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 2703: send stdout dump to coqide when an error occurs.Gravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14998 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coq_makefile: Add of extra options by defaultGravatar pboutill2012-02-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14997 85f007b7-540e-0410-9357-904b9bb8a0f7
* Univ: correct compare_neq (fix #2703)Gravatar letouzey2012-02-27
| | | | | | | | | | | | | | The earlier version was a bit too quick to answer <= while strict constraints could still appear from remaining universes to explore. Typical situation: compare u v when u <= v and u <= w < v. Encountering u <= v isn't enough to conclude yet... This means that kernels from r13719 to now in trunk, and from r13735 to now in 8.3 (including 8.3pl{1,2,3}) couldn't accurately detect universe inconsistencies, leading to potential proofs of False! Oups, sorry... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14993 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implement the substitution function for global options. Fixes anomaly in ↵Gravatar msozeau2012-02-23
| | | | | | ssreflect compilation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14991 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)Gravatar letouzey2012-02-22
| | | | | | | In addition to #2683, this also prevent Vernac.End_of_input exceptions when a buffer ends with one of the new delimiters -+*{}. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14989 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use a heuristic to not simplify equality hypotheses remaining after ↵Gravatar msozeau2012-02-20
| | | | | | | | dependent induction if they don't look really trivial. We still are making a choice though. Fixes bug #2712. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14988 85f007b7-540e-0410-9357-904b9bb8a0f7
* - changing minimal version for OCaml: Coq uses Filename.dirsep that is ↵Gravatar notin2012-02-20
| | | | | | | | available from OCaml 3.11.2 (see bug #2707) - fixing outdated address for Coq Club git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct application of head reduction.Gravatar msozeau2012-02-20
| | | | | | | | Fix a regression in subtac_pretyping, avoiding application of bidirectional application checking in case the return type is a subset (bad interaction with typeclass overloading). Should be done only on constructor applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14985 85f007b7-540e-0410-9357-904b9bb8a0f7
* Document the [unify] tactic.Gravatar msozeau2012-02-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14984 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of space after "Notation" or "where", add missing keywords.Gravatar msozeau2012-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14983 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid retrying uncessarily to prove independent remaining obligations in ↵Gravatar msozeau2012-02-15
| | | | | | Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14982 85f007b7-540e-0410-9357-904b9bb8a0f7
* Avoid unnecessary normalizations w.r.t. evars in Program.Gravatar msozeau2012-02-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14981 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 18:55:27 +0000