aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacintern.ml
AgeCommit message (Expand)Author
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2013-05-12Use the Hook module here and there.ppedrot
2013-05-10Removing Gmap from Tacinterp.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-04-22code simplifications concerning Summaryletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
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-18Modulification of Labelppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 00:40:43 +0000