aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Collapse)Author
2017-02-07Extraction: fix complexity issue #5310Pierre Letouzey
A double call to pp_module_type inside Ocaml.pp_specif was causing an complexity blowup when pretty-printing heavily modular extracted code. I wasn't able to figure out why this double call is there. It could be the leftover of some intermediate work in 2007 before commit 350398eae (which introduced global printing phases Pre/Impl/Intf). Anyway I'm reasonably sure that today these two pp_module_type calls produce the exact same pretty-printed signature (even if there's a large bunch of imperative states around). Moreover, this duplicated signature is actually slightly wrong: when we alias a module M with a unambiguous name like Coq__123, the type of Coq__123 should not be an exact copy of the type of M, but rather a "strengthened" version of it (with equality between inductive types). So the best solution is now to use this funny feature of OCaml introduced in 3.12 : module Coq__123 : module type of struct include M end This "module type of struct include" is slightly awkward, but short, correct, and trivial to produce :-). And I doubt anybody will object to the (rare) use of some 3.12 features in extracted code of 2017...
2016-12-07ssrmatching: fix iter_constr_LR iterator wrt ProjEnrico Tassi
2016-12-05ssrmatching: handle primite projections (fix: #5247)Enrico Tassi
2016-12-02Fixing printers for pr_auto_using and pr_firstorder_using.Hugo Herbelin
2016-11-24Lazily load constants in micromega (bug #5134).Guillaume Melquiond
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
Was PR#331: Solve_constraints and Set Use Unification Heuristics
2016-10-28Merge remote-tracking branch 'github/pr/319' into v8.6Maxime Dénès
Was PR#319: More error tagging, try to fix bug 5135
2016-10-25Merge commit 'a799600' into v8.6Maxime Dénès
Was PR#334: Fix bug 5031 : should not be an anomaly
2016-10-25That Function is unable to create a Fixpoint equation is a user problem,Yves Bertot
not an anomaly
2016-10-24ssrmatching: fix interpretation of rpatternEnrico Tassi
2016-10-22Renamings to avoid confusion deprecating old namesMatthieu Sozeau
reconsider_conv_pbs -> reconsider_unif_constraints consider_remaining_unif_problems -> solve_unif_constraints_with_heuristics
2016-10-18[pp] Use more convenient pp API in ssrmatchingEmilio Jesus Gallego Arias
2016-10-18[pp] Add tagging function to all low-level printing calls.Emilio Jesus Gallego Arias
The current tag system in `Pp` is generic, which implies we must choose a tagging function when calling a printer. For console printing there is a single choice, thus this commits adds it a few missing cases.
2016-10-17Fix bug #5023: JSON extraction doesn't generate "for xxx".Pierre-Marie Pédrot
2016-09-29Ncring_initial: avoid a notation overridingPierre Letouzey
2016-09-29Extraction: ignore some useless stuff about universesPierre Letouzey
2016-09-28Ring_theory: avoid overriding a few notationsPierre Letouzey
2016-09-28Adding interface files to Nsatz ML files.Pierre-Marie Pédrot
2016-09-26Fast russian peasant exponentiation in Nsatz.Pierre-Marie Pédrot
2016-09-26Monomorphizing various uses of arrays in Nsatz.Pierre-Marie Pédrot
2016-09-26Partial fix for bug #5085: nsatz_compute stack overflows.Pierre-Marie Pédrot
This fixes the stack overflow part of the bug, even if the tactic is still quite slow. The offending functions have been written in a tail-recursive way.
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
One of them revealed a true bug.
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
esprit d'escalier : is now also fixed for R
2016-09-08Fix Bug #5073 : regression of micromega pluginFrédéric Besson
The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
2016-09-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-07micromega : more robust generation of proof termsFrédéric Besson
- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
2016-09-03Fixing what is probably a typo in Strict Proofs mode (#5062).Hugo Herbelin
2016-09-02Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-01Fixed Bug #5003 : more careful generalisation of dependent terms.Frédéric Besson
2016-08-31Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.Frédéric Besson
If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
2016-08-30plugin micromega : nra also handles non-linear rational arithmetic over Q ↵Frédéric Besson
(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
2016-08-30micromega cache files are now hidden files (cf #4156)Frédéric Besson
csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache
2016-08-10Make it a bit more obvious when variables are of type unit.Guillaume Melquiond
2016-08-09Reduce warning noise when compiling the standard library.Guillaume Melquiond
2016-07-18Fix bug #4923: Warning: appcontext is deprecated.Pierre-Marie Pédrot
2016-07-13Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-07Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-07-06improved complexity in nsatzthery
we use a hashtable to reduce the complexity of creating a duplicate-free list.
2016-07-06Bug Fixes : 4851 4858 4880 for nsatzthery
the function in_ideal of ideal.ml supposes the list of polynomials does not contain zero and is duplicate free. I force this invariant in the call of in_ideal in nsatz.ml4 the function clean_pol returns the reduced list plus a list of booleans that indicates which polynomials have been deleted the function expand_pol translates back the certificate of the reduced to list to the complete list thanks to the list of booleans. The fix is quadratic with respect to the input list which should be ok for reasonable usage of nsatz. If there is some performance issue we could improve the in_pol function.
2016-07-05Revert "Merge remote-tracking branch 'github/pr/229' into trunk"Maxime Dénès
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
2016-07-05Bug fix : variable capture in ltac code of Nsatzthery
changing set (x := val) into let x := fresh "x" in set (x := val)
2016-07-04Merge remote-tracking branch 'github/pr/229' into trunkMaxime Dénès
Was PR#229: Bytecode compilation in a new 'make byte' rule apart from 'make world'
2016-07-04congruence: Restrict refreshing to SetMatthieu Sozeau
Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
2016-07-04congruence: remove casts of indexed termsMatthieu Sozeau
This fixes the end of bug #4069, provoked by a use of unshelve refine which introduces a cast.
2016-07-04congruence/univs: properly refresh (fix #4609)Matthieu Sozeau
In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.
2016-07-03rename toplevel/cerror.ml into explainErr.ml (too close to the new ↵Pierre Letouzey
lib/cErrors.ml)
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Pierre Letouzey
module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 10:04:07 +0000