aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-04-02A debug printer for Evd.Filter.tPierre Boutillier
2014-04-02Add a test case for bug 3251Jason Gross
It was closed in 5b39c3535f7b3383d89d7b844537244a4e7c0eca.
2014-04-02STM: be more resilient to explicit Back + Sideff commands (closes: 3251)Enrico Tassi
2014-04-02Fix Bug 3131 + Really drop mentions of info in refman.Pierre Boutillier
2014-04-02Fix Bug 3217Pierre Boutillier
Normalize the term to see if there are arguments to daclare implicits only if at least one argument occurs in the non normal form
2014-04-02Better error message when found more than once object of name ...Pierre Boutillier
2014-04-01Evars introduced by Proofview refining are flagged as GoalEvar. For somePierre-Marie Pédrot
reasons, some code depends on it.
2014-04-01Updated debugging printersHugo Herbelin
2014-04-01Propagating conversion_problem towards (postponed) evar/evar problems.Hugo Herbelin
Incidentally simplifies where evar/evar problems are treated (in evar_define and imitate rather than solve_simple_eqn).
2014-04-01Fixing bug #2900 (evar/evar unif was supposed to be treated inHugo Herbelin
solve_simple_eqn but in case the second evar was hidden behind a local variable, it arrived in evar_define and imitate, wrongly assuming progress).
2014-03-31Removing the Change_evar refiner rule.Pierre-Marie Pédrot
2014-03-31Removing dead code in Tactics.Pierre-Marie Pédrot
2014-03-28Using the new refine interface to define ML tactics.Pierre-Marie Pédrot
2014-03-28Lighter interface for creating refining tactics.Pierre-Marie Pédrot
2014-03-28Newline on -slash warning in coqdep.Pierre-Marie Pédrot
2014-03-28Define Tactics.bring_hyps in the new monad.Pierre-Marie Pédrot
2014-03-27Removing tactic compatibility layer from Eqdecide.Pierre-Marie Pédrot
2014-03-27Cosmetic changes in Equality.Pierre-Marie Pédrot
2014-03-26Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer in Equality.Pierre-Marie Pédrot
2014-03-26Removing Tacmach compatibility layer in Inv.Pierre-Marie Pédrot
2014-03-26Removing tactic compatibility layer from Inv.Pierre-Marie Pédrot
2014-03-26STM: when an error occurs in a worker send back a bunch of statesEnrico Tassi
In this way when the user fixes the script only a small part of the broken proof has to be recomputed on master. The density of states sent back decreases as they get far from the error. I.e. counting from the error, the worker sends back states at distance 0 1 2 3 5 7 10 14 19 26 35 47...
2014-03-26CoqIDE: better error reporting for Qed on incomplete proofEnrico Tassi
2014-03-26test for apply + TC resolutionEnrico Tassi
2014-03-26Adding an interface to Eqdecide and putting the grammar rules in a dedicatedPierre-Marie Pédrot
file.
2014-03-26Moving some tactic code to the new engine.Pierre-Marie Pédrot
2014-03-24Revert "Makefile: the initial build of grammar.cma is now directory-driven"Pierre Letouzey
This reverts commit f694544d016b085b3cd10007b9f7716ae2c3b022. This commit was wrong, since (at least) the highparsing part depends on the toplevel directory. I still didn't had time to fix that, so in the meantime let's revert it.
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-20Slightly more efficient Array.smartmap & related.Pierre-Marie Pédrot
2014-03-20Documenting the Print Strategy command.Pierre-Marie Pédrot
2014-03-19Adding a Print Strategy vernacular command. It allows to check thePierre-Marie Pédrot
transparent status of variables and constants.
2014-03-19Using non-normalized goals in tactic interpretation.Pierre-Marie Pédrot
2014-03-19Adding phantom types to discriminate normalized goals, and adding a way toPierre-Marie Pédrot
observe non-normalized goals.
2014-03-18Remove the -fno-defer-pop cflagJason Gross
According to http://caml.inria.fr/mantis/view.php?id=6346, this flag causes ocamlc to fail on the latest version of xcode, because clang now errors on -fno-defer-pop. According to the same issue, -fno-defer-pop is required for computed gotos if you're using gcc 1.xx, but not gcc 3.4.0 nor 4.4.7 (nor presumably other reasonably modern versions of gcc). I haven't actually tested this, as I don't have a mac, but it's a relatively small change. Signed-off-by: Pierre Boutillier <pierre.boutillier@ens-lyon.org>
2014-03-18Printing backtraces in coqchk while in debug mode.Pierre-Marie Pédrot
2014-03-18Fixing checker with respect to new kernel name structure and hashmaps.Pierre-Marie Pédrot
Some wrong generic equalities and hashes were removed too.
2014-03-18STM: make the slave start from the most recent known stateEnrico Tassi
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-17Evarconv: exact_ise_stack looks to stack head before bodies or branchesPierre Boutillier
the order of the inspection is a "random" choise but going back to the old behavior makes the compilation of ssreflect/rat.v 5 times faster ...
2014-03-17Fix test-suite 2255.vPierre Boutillier
2014-03-16consider_remaining_unif_problems respects Conv_oraclePierre Boutillier
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
no particular purpose.
2014-03-13nanoPG: better copy/pasteEnrico Tassi
2014-03-13fix compilation with ocaml < 4Enrico Tassi
2014-03-13STM: perspective (tell the scheduler what the user sees)Enrico Tassi
2014-03-13Stateid: export a Set moduleEnrico Tassi
2014-03-13STM: move out a couple of submodulesEnrico Tassi
These modules are not as reusable as one may want them to be, but moving them out simplifies a little STM.
2014-03-12fake_ide: fix compilationEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:09:46 +0000