aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hipattern.ml
Commit message (Expand)AuthorAge
* [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
* - Réintroduction d'un parseur de pattern (q_constr.ml4) à usage deGravatar herbelin2006-03-22
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Types inductifs parametriquesGravatar mohring2005-11-02
* Nouvelle en-têteGravatar herbelin2004-07-16
* code obsoleteGravatar herbelin2004-03-11
* Ground Update.Gravatar corbinea2003-06-20
* Ground and CCsolve updatesGravatar corbinea2003-05-25
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* Enhancement of the Ground tactic, addition of GTauto and GIntuition.Gravatar corbinea2003-05-07