aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
Commit message (Expand)AuthorAge
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* Tweak comments to fix ocamldoc errorsGravatar mrmr19932018-03-05
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.Gravatar Maxime Dénès2018-01-22
|\
| * Let dtauto recognize '@sigT A (fun _ => B)' as a conjunctionGravatar Jasper Hugunin2018-01-17
* | Use let-in aware prod_applist_assum in dtauto and firstorder.Gravatar Jasper Hugunin2018-01-17
|/
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Getting rid of pf_matches in Hipattern.Gravatar Pierre-Marie Pédrot2017-12-07
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#716: Don't double up on periods in anomaliesGravatar Maxime Dénès2017-06-06
|\
* \ Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...Gravatar Maxime Dénès2017-06-05
|\ \
| | * Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| |/ |/|
* | Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\ \
| | * Using a more explicit algebraic type for evars of kind "MatchingVar".Gravatar Hugo Herbelin2017-05-31
* | | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| |/ |/|
| * tactics cleanup: remove constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\
| * Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ |/|
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Removing the Q_constr file.Gravatar Pierre-Marie Pédrot2016-06-05
* Moving Hipattern to a regular ML file.Gravatar Pierre-Marie Pédrot2016-06-05