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
2020-10-10
Add location in existential variable names (CEvar/GEvar).
Hugo Herbelin
2020-10-10
Adding and using locations on identifiers in constr_expr where they were miss...
Hugo Herbelin
2020-07-06
Primitive persistent arrays
Maxime Dénès
2020-03-31
Include review suggestions
Gaëtan Gilbert
2020-03-31
Try only using TC for conversion in cominductive (not great but let's see)
Gaëtan Gilbert
2020-03-19
[declare/lemmas] Make inference hook exception-free
Emilio Jesus Gallego Arias
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-11
Reinforcing the role of type "typing_constraint".
Hugo Herbelin
2019-12-18
Merge PR #6090: Implement open recursion in the pretyper
Enrico Tassi
2019-12-17
Type pretyping is part of the open recursion
Pierre-Marie Pédrot
2019-12-17
Exporting the open-recursion style API.
Pierre-Marie Pédrot
2019-12-16
Pretyping.check_evars: make initial evar map optional
Gaëtan Gilbert
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-01
Allowing Set to be part of universe expressions.
Hugo Herbelin
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
[next]
