aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge PR #6824: Remove deprecated options related to typeclasses.Gravatar Maxime Dénès2018-03-06
|\
* \ Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"Gravatar Maxime Dénès2018-03-06
|\ \
* \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \
* \ \ \ Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monadGravatar Maxime Dénès2018-03-05
|\ \ \ \
| | | | * Remove deprecated options related to typeclasses.Gravatar Théo Zimmermann2018-03-04
| |_|_|/ |/| | |
| * | | tactics: export e_reduct_in_conclGravatar Enrico Tassi2018-03-04
* | | | Merge PR #6791: Removing compatibility support for versions older than 8.5.Gravatar Maxime Dénès2018-03-04
|\ \ \ \ | |/ / / |/| | |
* | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \ \ \
* \ \ \ \ Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret...Gravatar Maxime Dénès2018-03-04
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \ \ \ \
| | | | | | * [compat] Remove "Injection L2R Pattern Order"Gravatar Emilio Jesus Gallego Arias2018-03-03
| | | | * | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
| | | | | |/ | | | | |/|
* | | | / | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| |_|_|/ / |/| | | |
| | * | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4.Gravatar Hugo Herbelin2018-03-01
| |/ / / |/| | |
| | * | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| |/ / |/| |
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| * proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/
* Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Maxime Dénès2018-02-19
|\
* | apply_type: add option "typecheck" passed down to refineGravatar Enrico Tassi2018-02-16
| * [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
|/
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
* Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.Gravatar Maxime Dénès2018-01-31
|\
* \ 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
|/ /
| * Cleanup name-binding structure for fresh evar name generation.Gravatar Pierre-Marie Pédrot2018-01-02
* | Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
|/
* Merge PR #6493: [API] remove large file containing duplicate interfacesGravatar Maxime Dénès2017-12-29
|\
| * [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
|/
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
* Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Gravatar Maxime Dénès2017-12-18
|\
| * [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* | Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\ \
* \ \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \ \
* | | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| |_|/ |/| |
| | * Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| | * Remove deprecated option Dependent Propositions Eliminiation.Gravatar Théo Zimmermann2017-12-11
| |/ |/|
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* | Getting rid of pf_matches in Hipattern.Gravatar Pierre-Marie Pédrot2017-12-07
|/
* Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...Gravatar Maxime Dénès2017-11-30
|\
| * In injection/inversion, consider all template-polymorphic types as injectable.Gravatar Hugo Herbelin2017-11-28
* | Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* | When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* | Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* | Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #486: Make some functions on terms more robust w.r.t new term constr...Gravatar Maxime Dénès2017-11-24
|\
| * Make one more function robust in term_dnet.mlGravatar Maxime Dénès2017-11-23
| * Make some functions on terms more robust w.r.t new term constructs.Gravatar Maxime Dénès2017-11-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 05:47:00 +0000