aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-11-10Fix #3282: VM confused by let bindings in fixpoints.Maxime Dénès
I'm afraid this fix is a bit heuristic, but it seems to generate correct code in all cases.
2014-11-10Better printing of dynlink errors in native compiler.Maxime Dénès
2014-11-10Plug the dynamic tags in the Richpp mechanism.Pierre-Marie Pédrot
2014-11-10Adding a dynamic tag type in Pp.Pierre-Marie Pédrot
2014-11-10Replugging hints in rewriting strategies.Pierre-Marie Pédrot
2014-11-10Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).Pierre-Marie Pédrot
2014-11-09Fixing bug #3803.Pierre-Marie Pédrot
The Info layer was setting the required evarmap too eagerly, making the tclWITHHOLE tactical accept terms with holes. The logging facility is now inside the tclWITHHOLES.
2014-11-09Removing the unused boolean flag from the move tactic implementation.Pierre-Marie Pédrot
2014-11-09Removing a unused boolean in the TacMove node of tacexpr AST.Pierre-Marie Pédrot
2014-11-09Adding test for bug 3792.Pierre-Marie Pédrot
2014-11-09Fixing bug #3792.Pierre-Marie Pédrot
Pretyping of [if] cases was missing a convertibility check with the ambient type constraint, and just dropped it. This was making the pretyper construct ill-typed terms.
2014-11-09new: Optimize Proof, Optimize HeapEnrico Tassi
- drops all Defined entries from the evar map (applying the subst to the initial evar and the undefined evars types). - call Gc.compact Now the question is: where should these two commands be documented?
2014-11-08Follow up to experimental eager evar unification in bcba6d1bc9:Hugo Herbelin
Observing that systematic eager evar unification makes unification works better, for instance in setoid rewrite (ATBR, SemiRing.v), we add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put to true only in Rewrite.rewrite_core_unif_flags (empirically, this makes the "rewrite" from rewrite.ml working again on examples which were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
2014-11-08Fixing a bug in change of subst_defined_metas in bcba6d1bc9f769da:Hugo Herbelin
One missing evar was making the whole substitution fail. The bug actually existed a priori also in the case where only metas are substituted (i.e. before bcba6d1bc9f769da), leading to limit the number of situations where it could be effectful. This fixes current failures of RelationAlgebra and CFGV.
2014-11-08Continuing 3741c46fe134 on reporting ltac error.Hugo Herbelin
- Do use the flag for_ml for distinguishing coq level and ml level ltac definitions. - Skip ML call from the trace. There are still differences from 8.4 and trunk. For instance on: Ltac f x := refine x. Goal False. f I. 8.4 says: In nested Ltac calls to "f" and "x" (with x:=I), last term evaluation failed. Error: The term "I" has type "True" while it is expected to have type "False". trunk says: In nested Ltac calls to "f" and "refine <genarg:uconstr>", last call failed. Error: The term "I" has type "True" while it is expected to have type "False". Maybe we would like a mix of both (besides the printing of a non-elegant "<genarg:uconstr>)?
2014-11-08Compatibility with 8.4 in the heuristic used to build the inductionHugo Herbelin
hypothesis when indices also occur among parameters. This solves current failure of PersistentUnionFind.
2014-11-08Test #3655 was failing due to an anomaly. Now it rather has to failHugo Herbelin
normally, so failure is now detected by removing the "Fail".
2014-11-08Test fixed by PMP's commits from Oct 21.Hugo Herbelin
2014-11-07Fixing doc of Functional Induction.Hugo Herbelin
2014-11-07Fixing Functional Induction when applied to an alias (reference manualHugo Herbelin
for Functional Induction was failing because of minus now an alias). Knowing that minus is an alias for Sub.nat, there are still two bugs in Functional Induction (Pierre or Julien?): "Functional Scheme minus_ind := Induction for minus Sort Prop." is failing when Nat is not imported. "functional induction (minus n m)" is failing because looking for sub_ind while the scheme is named minus_ind.
2014-11-07Granting #3717 (more informative error message on missing arguments for ↵Hugo Herbelin
functional induction).
2014-11-07Test for #3675 on primitive projections.Hugo Herbelin
2014-11-07Fixing #3562 ("as" in "destruct" expects either a disjunctiveHugo Herbelin
intropattern or a bound ltac variable).
2014-11-07Test for #3542 fixed some time ago.Hugo Herbelin
2014-11-07doc: version number in cover.html + updates in coq.inria.fr stylePierre Letouzey
2014-11-07Removing the legacy intro tactic code.Pierre-Marie Pédrot
2014-11-07Print [rename] tactic properly in info trace.Arnaud Spiwack
Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).
2014-11-06Consequence of changing the definition of Nat.shiftl and Nat.shiftr.Hugo Herbelin
2014-11-06Restoring clear_flag (thanks a lot to jonikelee to notice it).Hugo Herbelin
2014-11-06Optimizing when to clear generalized hypotheses in destruct.Hugo Herbelin
Removing blocking of generalization on destructed hypothesis introduced on Nov 2. It was a bad idea as shown by bug #3790 on eliminating v:Vector n, keeping an equality.
2014-11-06Dependency bug in using eqn for destruct.Hugo Herbelin
2014-11-06Test for bug #3723 and #3787 on reinitialization of empty camlp4/5 levels.Hugo Herbelin
2014-11-06Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)Hugo Herbelin
by hopefully computing the right position where to reinit an empty level. Also removing obsolete comment.
2014-11-06Removing "destruct" test not yet working.Hugo Herbelin
2014-11-06Fixing compilation (name of module Richprinter) I partially feelHugo Herbelin
responsible about.
2014-11-05lib/RichPp: Rename into Richpp.Yann Régis-Gianas
printing/RichPrinter: Rename into Richprinter. printing/{ppvernac, ppconstr, pptactic}: Rename RichPp into Richpp. printing/Richprinter: Cosmetics.
2014-11-05lib/richPp: Fix a bug related to the compatibility with ocaml 3.12Yann Régis-Gianas
- The previous version of this module was using a feature of the Format module of ocaml 4.01. - Add comments.
2014-11-05printing/Ppvernac: Fix missing keyword tagging on theorem introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Fix missing keyword tagging on definition introducers.Yann Régis-Gianas
2014-11-05printing/Ppvernac: Cosmetics.Yann Régis-Gianas
2014-11-05Writing the raw introduction tactic in the new monad.Pierre-Marie Pédrot
2014-11-04ide/Xmlprotocol: Cosmetics.Yann Régis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04lib/richPp: Cosmetics.Regis-Gianas
2014-11-04printing/Ppannotation: New annotation for tactic syntactic objects.Regis-Gianas
printing/Pptactic: Tag tactics pretty-printing. printing/Ppvernac: Use the relevent Pptactic pretty-printer. printing/RichPrinter: Publish two new services.
2014-11-04printing/Pptactic.Make: New.Regis-Gianas
- Functorize with respect to the pretty-printer for constr. - Include the application of Make to Ppconstr at toplevel in order to preserve previous behavior.
2014-11-04printing/Pptacticsig: New signature for tactic pretty-printers.Regis-Gianas
printing/Pptactic: Use it.
2014-11-04lib/Ppconstr: Cosmetics.Regis-Gianas
2014-11-04Rebase artefact.Regis-Gianas
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:06:57 +0000