index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
pretyping.mli
Age
Commit message (
Expand
)
Author
2019-05-28
[elaboration] Bidirectionality hints
Maxime Dénès
2019-03-27
[geninterp] Track polymorphic status in tactic interpretation.
Emilio Jesus Gallego Arias
2019-02-05
Make Program a regular attribute
Maxime Dénès
2018-11-21
Make initial evar map argument to check_evars_are_solved optional.
Gaëtan Gilbert
2018-11-16
Remove the implicit tactic feature following #7229.
Pierre-Marie Pédrot
2018-10-03
[pretyper] Less imperative passing of the evar_map, part I.
Emilio Jesus Gallego Arias
2018-09-10
Moving part of pretyping dealing with ltac and renaming in new module GlobEnv.
Hugo Herbelin
2018-05-08
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-02-28
[econstr] Continue consolidation of EConstr API under `interp`.
Emilio Jesus Gallego Arias
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-19
pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)
Enrico Tassi
2017-11-28
Merge PR #1033: Universe binder improvements
Maxime Dénès
2017-11-26
[api] Remove aliases of `Evar.t`
Emilio Jesus Gallego Arias
2017-11-25
Fix interpretation of global universes in univdecl constraints.
Gaëtan Gilbert
2017-11-22
[api] A few more minor deprecation notices.
Emilio Jesus Gallego Arias
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-10-25
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
2017-09-08
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-08-01
Remove understand_tcc_evars.
Maxime Dénès
2017-08-01
Move type_uconstr to Tacinterp.
Maxime Dénès
2017-08-01
Remove understand_judgment and understand_judgment_tcc.
Maxime Dénès
2017-08-01
Remove allow_anonymous_refs.
Maxime Dénès
2017-08-01
Remove pure_open_constr (now open_constr)
Maxime Dénès
2017-08-01
Move glob_constr_ltac_closure to evar_refiner.
Maxime Dénès
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-09
A fix to #5414 (ident bound by ltac names now known for "match").
Hugo Herbelin
2017-05-25
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-03
Generalizing the tactic-in-term embedding to any generic argument.
Pierre-Marie Pédrot
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-04-07
Merge branch 'master' into econstr
Pierre-Marie Pédrot
2017-03-23
Ensuring static invariants about handling of pending evars in Pretyping.
Pierre-Marie Pédrot
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Cleaning up interfaces.
Pierre-Marie Pédrot
2017-02-14
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
Ltac now uses evar-based constrs.
Pierre-Marie Pédrot
2017-02-14
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
Pretyping API using EConstr.
Pierre-Marie Pédrot
2016-11-18
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-11-07
More explicit name for status of unification constraints.
Maxime Dénès
2016-10-02
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-28
Fix bug #4723 and FIXME in API for solve_by_tac
Matthieu Sozeau
2016-09-15
Untangling Tacexpr from lower strata.
Pierre-Marie Pédrot
2016-09-08
Unplugging Tacexpr in several interface files.
Pierre-Marie Pédrot
2016-06-18
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-16
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-15
Allow `Pretyping.search_guard` to not check guard
Arnaud Spiwack
2016-05-04
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-03-25
Moving type_uconstr to Pretyping.
Pierre-Marie Pédrot
2016-03-20
Making Evarutil independent from Reductionops.
Pierre-Marie Pédrot
[next]
