index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
proofs
/
evar_refiner.ml
Age
Commit message (
Expand
)
Author
2019-11-21
[coq] Untabify the whole ML codebase.
Emilio Jesus Gallego Arias
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-03-27
[geninterp] Track polymorphic status in tactic interpretation.
Emilio Jesus Gallego Arias
2019-02-08
[evarconv] New flag handling for unifier
Matthieu Sozeau
2019-02-05
Make Program a regular attribute
Maxime Dénès
2018-11-19
Rename TranspState into TransparentState.
Pierre-Marie Pédrot
2018-11-19
Move transparent_state to its own module.
Pierre-Marie Pédrot
2018-11-16
Remove the implicit tactic feature following #7229.
Pierre-Marie Pédrot
2018-04-13
Evar maps contain econstrs.
Gaëtan Gilbert
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-10-25
[general] Remove Econstr dependency from `intf`
Emilio Jesus Gallego Arias
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-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-04-25
[location] Make location optional in Loc.located
Emilio Jesus Gallego Arias
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Moving printing code from Evd to Termops.
Pierre-Marie Pédrot
2017-02-14
Removing various compatibility layers of tactics.
Pierre-Marie Pédrot
2017-02-14
Hints API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Pretyping API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Evarconv API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Termops 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-08-19
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-07-13
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-07-13
Fixing printing of evar name in an error message of instantiate.
Hugo Herbelin
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-03-20
Extruding the code for the Existential command from Proofview.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-04-23
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-01-12
Update headers.
Maxime Dénès
2014-09-12
Uniformisation of the order of arguments env and sigma.
Hugo Herbelin
2014-09-12
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-08-07
Better structure for Ltac pretyping environments.
Pierre-Marie Pédrot
2014-08-06
[uconstr]: use a closure instead of eager substitution.
Arnaud Spiwack
2013-12-17
Removing the need of evarmaps in constr internalization.
Pierre-Marie Pédrot
2013-09-18
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-06-22
Generalizing the use of maps instead of lists in the interpretation
ppedrot
2013-05-09
A uniformization step around understand_* and interp_* functions.
herbelin
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 12)
letouzey
2013-02-17
Added propagation of evars unification failure reasons for better
herbelin
2013-01-29
Renaming evar_env/evar_unfiltered_env into evar_filtered_env/evar_env
herbelin
2012-11-25
Monomorphization (proof)
ppedrot
2012-09-14
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
This patch removes unused "open" (automatically generated from
regisgia
2012-08-08
Updating headers.
herbelin
2012-05-29
Glob_term now mli-only, operations now in Glob_ops
letouzey
[next]
