aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
AgeCommit message (Expand)Author
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-05-30Removing a useless location in ltac trace mechanism.ppedrot
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
2013-05-28Fixing debug of empty Ltac matching goal.ppedrot
2013-05-28Pushing lazy lists into Ltac. Now, the control flow is explicitppedrot
2013-05-24Code cleaning in Matching.ppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-17Revised the Ltac trace mechanism so that trace breaking due toherbelin
2013-01-29Fixed #2970 (made that remember's eqn name is interpretable as an ltac var).herbelin
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-11-25Monomorphization (tactics)ppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06cosmetic concerning interp of TacShowHypsletouzey
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Adapt pieces of code needing -rectypesletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-08Updating headers.herbelin
2012-08-05Dump references in reduction tacticspboutill
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-04Replacing some str with strbrkppedrot
2012-06-01Cleaning Pp.ppnl useppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey
2012-05-29slim down a bit genarg.ml (pr_intro_pattern forgotten there)letouzey
2012-05-29Pattern as a mli-only file, operations in Patternopsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 16:20:49 +0000