aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.mli
Commit message (Expand)AuthorAge
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* Correcting [build_discriminator] to make the test-suite passGravatar amblaf2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Equality cleanup: remove constr_of_globalGravatar Matthieu Sozeau2017-05-29
* Stopping injection not to work on discriminable atoms (see #4890).Gravatar Hugo Herbelin2017-05-17
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Exporting build_selector, a component of discriminate, for use in congruence.Gravatar Hugo Herbelin2016-03-05
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing tactic compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Clean up a warning.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Safer, though ad hoc, approach to re-interpretation of the argument ofGravatar herbelin2009-12-28
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* adding an option functional_induction_rewrite_dependent to make functional in...Gravatar jforest2009-12-16
* Updated compatibility for rewriting equality proofs that are dependentGravatar herbelin2009-12-12
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 00:16:12 +0000