aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-10-17Vernac.ml: inlining read_vernac_file within load_vernac.Hugo Herbelin
Also renaming vernac_com into interp_vernac and eval_expr into process_vernac to clarify that it does side-effects (on the contrary of Stm.interp/Vernacentries.interp).
2016-10-17Grouping checks about commands together.Hugo Herbelin
2016-10-17Vernac.ml: parenthesizing a side-effect.Hugo Herbelin
Moving set_formatter_out_channel where it naturally closes the corresponding opening set_formatter_output_functions.
2016-10-17Factorizing two instances of load_vernac.Hugo Herbelin
2016-10-17Passing chan_beautify functionally rather than by side-effect.Hugo Herbelin
2016-10-17Applying Emilio's suggestion to simplify type of eval_expr.Hugo Herbelin
This is not fully satisfactory though since we would not like to have "eval_expr" depending on a parsing/lexing/comments state... but it does because of eval_expr possibly printing the vernac expression given to it.
2016-10-17More on making the lexer more functional (continuing b8ae2de5 andHugo Herbelin
8a8caba3). - Adding cLexer.current_file to the lexer state, i.e. making it a component of the type "coq_parsable" of lexer state (it was forgotten in b8ae2de5 and 8a8caba3). - Inlining save_translator/restore_translator which have now lost most of their substance.
2016-10-17Removing export of location_table outside of cLexer.Hugo Herbelin
It was not used any more by coqdoc since b8194b22 (Dec 2010). The table is now only part of the lexer function closure (and only in the camlp5 case).
2016-10-17Fix compilation with camlp4 broken in 8a8caba3.Hugo Herbelin
2016-10-17Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-17Fix output test for module qualification.Pierre-Marie Pédrot
The output was embedding local paths from my machine.
2016-10-17Fix previous commit.Pierre-Marie Pédrot
I've messed up with parts of the compatibility files I had to commit.
2016-10-17Merge PR #300 into v8.6Pierre-Marie Pédrot
2016-10-17Example illustrating non-local inference of the default type of impossible ↵Hugo Herbelin
branches (see PR #323).
2016-10-17Merge PR #310 into v8.5Pierre-Marie Pédrot
2016-10-17Merge PR #310 into v8.6Pierre-Marie Pédrot
2016-10-17Test for bug #4874.Pierre-Marie Pédrot
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-10-16Fix bug #5141: Bogus message "Error: Cannot infer type of pattern-matching".Pierre-Marie Pédrot
We simply explicit that the type is actually referring to the return type, not to the type of the argument of the pattern-matching. Note that the heuristic could be enhanced so as to use the same code in both let-style and match-style pattern-matching, but I'm leaving this for another time.
2016-10-15Fix bug #5145: Anomaly: index to an anonymous variable.Pierre-Marie Pédrot
When printing evar constraints, we ensure that every variable from the rel context has a name.
2016-10-15Still a problem with debug auto printing.Hugo Herbelin
"msg_debug (mt())" is not identity, so we return back to how it was done in 8.4, contracting a repeated pattern-matching into one.
2016-10-15One more little bug in the output of "debug auto".Hugo Herbelin
Header was missing in last commit. One day, it would be nice to unify the display of "debug auto" and "debug eauto"...
2016-10-14Fix bug #5139: Anomalies should not be caught by || / try.Pierre-Marie Pédrot
There was a catch-all clause in the tclORELSE0 function. We now only catch noncritical exceptions.
2016-10-14Fixing printing of info_auto broken since 0091c528 (2014).Hugo Herbelin
2016-10-14Fixing English typography for colon.Hugo Herbelin
2016-10-14Using "simple apply" and "simple eapply" in the trace of auto.Hugo Herbelin
This is more precise and probably clearer (see e.g. thread "Understanding auto" on coq-club).
2016-10-13Completing reverting generalization and cleaning of the return clause inference.Hugo Herbelin
Revert "Inference of return clause: giving uniformly priority to "small inversion"." This reverts commit 980b434552d73cb990860f8d659b64686f6dbc87.
2016-10-12Remove dead code in Environ.Pierre-Marie Pédrot
2016-10-12Merge PR #224 into v8.6Pierre-Marie Pédrot
2016-10-12Merge PR #289 into v8.6.Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Tentatively preparing to add changes specific to v8.7 (see PR #275).Hugo Herbelin
2016-10-12Little addition to 6eede071 for consistency of style in OrdersFacts.v.Hugo Herbelin
2016-10-12Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
This happens when recursive notations are used to define recursive notations.
2016-10-12Merge remote-tracking branch 'github/pr/286' into v8.5Maxime Dénès
Was PR#286: Fix the definition of if_then_else for tactics with multiple success.
2016-10-12Fix bug #5116: [Print Ltac] should be able to print strategies.Pierre-Marie Pédrot
2016-10-12Fix git recognition when in worktrees.Théo Zimmermann
git worktrees have a .git file instead of a .git directory. Using Sys.file_exists is a more general solution which gives true in both cases.
2016-10-12Fix bug #4958: [debug auto] should specify hint databases.Pierre-Marie Pédrot
2016-10-12Shorter message for "Test Asymmetric Patterns".Hugo Herbelin
But maybe it is that how the "Test" message is elaborated is not intuitive...
2016-10-12Merge remote-tracking branch 'git/bug5123' into v8.5Matthieu Sozeau
2016-10-12Fixing a few confusions on the name of the beautify flag.Hugo Herbelin
(It should apply also interactively.)
2016-10-11Fix test-suite file 5123 to fail in case of regressionMatthieu Sozeau
2016-10-11Merge remote-tracking branch 'github/bug4863' into v8.5Matthieu Sozeau
2016-10-11Fix bug #5123: mark all shelved evars unresolvableMatthieu Sozeau
Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
2016-10-11Reverting generalization and cleaning of the return clause inference in v8.6.Hugo Herbelin
The move to systematically trying small inversion first bumps sometimes as feared to the weakness of unification (see #5107). ---- Revert "Posssible abstractions over goal variables when inferring match return clause." This reverts commit 0658ba7b908dad946200f872f44260d0e4893a94. Revert "Trying an abstracting dependencies heuristic for the match return clause even when no type constraint is given." This reverts commit 292f365185b7acdee79f3ff7b158551c2764c548. Revert "Trying a no-inversion no-dependency heuristic for match return clause." This reverts commit 2422aeb2b59229891508f35890653a9737988c00.
2016-10-11Fix for bug #4863, update the Proofview's env withMatthieu Sozeau
side_effects. Partial solution to the handling of side effects in proofview.
2016-10-10Fixing #5133 (error reporting delayed).Hugo Herbelin
I wrongly moved call to the function interpreting commands within a different try-with block in 8a8caba36e.
2016-10-10Add test file for #4416.Maxime Dénès
2016-10-10Fix #4416: - Incorrect "Error: Incorrect number of goals"Arnaud Spiwack
In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 18:22:20 +0000