aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-03-19More adaptations of pretyping/coercion to Program mode.msozeau
2012-03-19Fix bugs related to Program integration.msozeau
2012-03-19Hopefully complying with camlp5 < 6.00 syntaxherbelin
2012-03-19Bug 2709: Duplication in coqdoc index entriespboutill
2012-03-19RefMan: Environment variables description updatepboutill
2012-03-19Fixes bug: #2692 (Arguments/simpl off by 1)gareuselesinge
2012-03-19Arguments/simpl: allow ! even on non fixpointsgareuselesinge
2012-03-18Yet another subtlety with bug 2732: when several grammar rules of aherbelin
2012-03-18Removing redundant entry int_nelist and removing extra space whenherbelin
2012-03-18Fixing bug #2732 (anomaly when using the tolerance for writingherbelin
2012-03-14Fix merge and add missing file.msozeau
2012-03-14Fix merge.msozeau
2012-03-14Revise API of understand_ltac to be parameterized by a flag for resolution of...msozeau
2012-03-14Merge fixesmsozeau
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Integrated obligations/eterm and program well-founded fixpoint building to to...msozeau
2012-03-14Everything compiles again.msozeau
2012-03-14Second step of integration of Program:msozeau
2012-03-14Remove support for "abstract typing constraints" that requires unicity of sol...msozeau
2012-03-13A bit of cleaning: unifying push_rels and push_rel_context.herbelin
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-12Univ: avoid recording dummy universe constraints u<=u or u=uletouzey
2012-03-02Glob_term.predicate_pattern: No number of parameters with letins.pboutill
2012-03-02"Let in" in pattern hell, one more iterationpboutill
2012-03-02Noise for nothingpboutill
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2012-03-01Univ: a better Constraint.compareletouzey
2012-03-01Corrects the erroneous error message when trying to unfocus a fullyaspiwack
2012-03-01Removed a superfluous function in proof.mli. Preparing for incomingaspiwack
2012-03-01New version of recdef :jforest
2012-03-01various corrections in invfun due to a modification in inductionjforest
2012-02-29Univ: a faster is_leq test used when possibleletouzey
2012-02-29correcting a little bug in invfun.mljforest
2012-02-29correction of bug 2457jforest
2012-02-29Fix compilation of Constrintern...pboutill
2012-02-29RefMan update about match syntax.pboutill
2012-02-29In the syntax of pattern matching, the arguments of the inductive in the "in"pboutill
2012-02-29In the syntax of pattern matching, "in" clauses are patterns.pboutill
2012-02-29Vector: missing injection lemmas and better impossible branchespboutill
2012-02-29Bug 2703: send stdout dump to coqide when an error occurs.pboutill
2012-02-29Coq_makefile: Add of extra options by defaultpboutill
2012-02-27Univ: correct compare_neq (fix #2703)letouzey
2012-02-23Implement the substitution function for global options. Fixes anomaly in ssre...msozeau
2012-02-22Ide: sentences found by find_phrase_starting_at should be nonempty (fix #2683)letouzey
2012-02-20Use a heuristic to not simplify equality hypotheses remaining after dependent...msozeau
2012-02-20- changing minimal version for OCaml: Coq uses Filename.dirsep that is availa...notin
2012-02-20Correct application of head reduction.msozeau
2012-02-18Document the [unify] tactic.msozeau
2012-02-16Fix handling of space after "Notation" or "where", add missing keywords.msozeau
2012-02-15Avoid retrying uncessarily to prove independent remaining obligations in Prog...msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:29:53 +0000