aboutsummaryrefslogtreecommitdiff
path: root/tactics
AgeCommit message (Expand)Author
2013-03-14Embedded exns in LtacLocated and EvaluatedError satisfy Errors.noncriticalletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 11)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 10)letouzey
2013-03-12Hipattern : consider jmeq only when Logic.JMeq is loadedletouzey
2013-03-12Equality: avoid an anomaly about inj_pair2_eq_decletouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
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-29Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_envherbelin
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-18Modulification of nameppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Fixed a little inefficiency of "set/destruct" over a pattern. Nowherbelin
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-13Using library string functions.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-11-25Monomorphization (tactics)ppedrot
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-13Added a CString module.ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-31Change [Hints Resolve] to still accept constrs as argumentsmsozeau
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
2012-10-06still some more dead code removalletouzey
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-04Revert r15851 "En cours pour bug 2836".herbelin
2012-10-04Improving error message when abtraction over goal (abstract_list_allherbelin
2012-10-04En cours pour bug 2836herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-17 23:33:34 +0000