aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-02-25Tacinterp: remove the is_value check in Ltac's let-in.Arnaud Spiwack
It fixes micromega. It is frankly a mystery to me why psatz ever work. The semantics of Ltac's match is still fishy.
2014-02-25Tacinterp: fewer enterl still.Arnaud Spiwack
2014-02-25Tacinterp: fewer Proofview.Goal.enterl.Arnaud Spiwack
I'm trying to avoid unecessary construction of intermediate lists. Interpretation function don't modify the goals, they just need a goal in their context. Some care has to be given to the evar maps, though, as we can extract an outdated evar map from a goal (this is probably an undesirable feature, but significantly simplified the compatibility API). Also, Proofview.Goal.enter{,l} catch exceptions (and transfer the non-critical ones into errors of the tactics monad). So I had to do just that for every "enter" removed (I probably have been overprotective but it's better that way). Not as trivial a modification as it should, but it will hopefully go over well. It was much needed anyway.
2014-02-25Tacinterp: clean up.Arnaud Spiwack
2014-02-25Tacinterp: remove unnecessary return/bind pairs.Arnaud Spiwack
2014-02-25Fixing printing of only_parsing notations.Pierre-Marie Pédrot
2014-02-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: more efficient implementation of concat_map.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
2014-02-24IStream: change type of thunk, spare allocations.Arnaud Spiwack
Two changes: - 'a Lazy.t becomes unit -> 'a - 'a t becomes 'a u (the view type) This spares two Lazy.force, and leverages Lazy.lazy_from_fun. Considering Lazy.force is fairly slow, in particular because of the write-barrier, this should be beneficial.
2014-02-24IStream: remove a useless Obj.magic.Arnaud Spiwack
Lazy.lazy_from_val does almost the same thing as this Obj.magic. It makes some extra dynamic check, but it's frankly unlikely that it could be observed.
2014-02-24A view type for IStream.Arnaud Spiwack
View types are better practice than option types for pattern-matching. (Plus, they save a minute amount of allocations)
2014-02-24Ensuring that the module Stack is opaque inside Reductionops.Pierre-Marie Pédrot
2014-02-24make coqide-binaries does not build coqtop anymorePierre Boutillier
2014-02-24fixup complement FinPierre Boutillier
2014-02-24cbn understands ArgumentsPierre Boutillier
(excepts list of args that must be constructors
2014-02-24Simpl_behaviour becomes Reductionops.ReductionBehaviourPierre Boutillier
syntax mentionning simpl remains
2014-02-24Dead Code eliminationPierre Boutillier
2014-02-24Create Debug Unification optionPierre Boutillier
to dump states that Evarconv.eq_appr_x tries to unify.
2014-02-24Fix coqide build under MacOSPierre Boutillier
2014-02-24No more translation array <-> list in Reductionops.StackPierre Boutillier
2014-02-24Reductionops.Stack.strip* are ready to deal with ShiftPierre Boutillier
2014-02-24Reductionops.Stack.app_node is secretPierre Boutillier
2014-02-24app_node, stack, state printersPierre Boutillier
2014-02-24Stack operations of Reductionops in Reductionops.StackPierre Boutillier
2014-02-24Fix grammatical mistake in error message (bug #3238)xclerc
2014-02-21More sharing in Logic, together with some code cleaning.Pierre-Marie Pédrot
2014-02-20Optimization in kernel/vars.ml: directly allocate a fixed-size block in thePierre-Marie Pédrot
subst1 case.
2014-02-17CoqIDE: when coqtop misbehaves kill it properly (no zombie)Enrico Tassi
2014-02-17[nanoPG]: emacs like copy/pasteEnrico Tassi
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
containing opaque grammar objects, it now contains a string representing the entry. In order to recover the entry from the string, the former must have been created with [Pcoq.create_generic_entry] or similar. This is guaranteed for entries generated by ARGUMENT EXTEND, and must be done by hand otherwise. Some plugins were fixed accordingly.
2014-02-14fast correction of bug #3234Julien Forest
2014-02-12TC: honor the use_typeclasses flag in pretypingEnrico Tassi
The coercion code was not seeing such flag and always trying to resolve type classes. In particular open_contr is pretyped without type classes.
2014-02-11Made Pre_env.lazy_val opaque.Pierre-Marie Pédrot
2014-02-10Timeout and Set Default Timeout fixed (closes: #3229)Enrico Tassi
2014-02-10STM: fix valid_id coming from Qed errorsEnrico Tassi
2014-02-10STM: when a worker is canceled mark the proof as brokenEnrico Tassi
2014-02-10STM: be conservative w.r.t. proofs containing global side effectsEnrico Tassi
2014-02-10fake_ide: ported to spawnEnrico Tassi
2014-02-10Tentative fixup for the previous commit. It seems I have broken somethingPierre-Marie Pédrot
nasty relating memory management triggering random segfaults. But this seemed really unlikely...
2014-02-09Small optimizations in Closure:Pierre-Marie Pédrot
1. Only apply last Zupdates 2. Better smartmap with state.
2014-02-08Less dependencies in Omega.Pierre-Marie Pédrot
2014-02-07FinFun.v: results about injective/surjective/bijective fonctions over finite ↵Pierre Letouzey
domains + Some extra results about NoDup, Fin.t, ...
2014-02-05Tactic extensions do not need to be classified by the STM, asPierre-Marie Pédrot
they never produce a VernacExtend entry.
2014-02-04The constructor tactic now returns several successes.Pierre-Marie Pédrot
2014-02-03Tracking memory misallocation by trying to improve sharing.Pierre-Marie Pédrot
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2014-02-03Allocation friendly map-handling functions in Dag.Pierre-Marie Pédrot
2014-02-02Fixing backtrace reporting.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:16:49 +0000