index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
proofs
/
refine.ml
Age
Commit message (
Expand
)
Author
2017-09-06
Fix a refine anomaly "Evar defined twice".
Pierre-Marie Pédrot
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-13
Dualize the unsafe flag of refine into typecheck and make it mandatory.
Pierre-Marie Pédrot
2017-06-13
Turn the default behaviour of the refine primitive into the safe one.
Pierre-Marie Pédrot
2017-06-06
Remove the Sigma (monotonous state) API.
Maxime Dénès
2017-05-25
Merge PR#608: Allow Ltac2 as a plugin
Maxime Dénès
2017-05-03
Generalizing the refine primitive so as to accept tactic arguments.
Pierre-Marie Pédrot
2017-04-25
[location] Remove Loc.ghost.
Emilio Jesus Gallego Arias
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2017-02-14
Removing compatibility layers in Retyping
Pierre-Marie Pédrot
2017-02-14
Proofview.Goal primitive now return EConstrs.
Pierre-Marie Pédrot
2017-02-14
Refine API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Making judgment type generic over the type of inner constrs.
Pierre-Marie Pédrot
2017-02-14
Unification API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Coercion API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Typing API using EConstr.
Pierre-Marie Pédrot
2017-02-14
Retyping API using EConstr.
Pierre-Marie Pédrot
2016-11-18
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-22
Renamings to avoid confusion deprecating old names
Matthieu Sozeau
2016-10-22
Unification constraint handling (#4763, #5149)
Matthieu Sozeau
2016-10-12
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-12
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-09-23
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-16
Adding variants enter_one and refine_one which assume that exactly one
Hugo Herbelin
2016-09-02
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-09-02
Merge branch 'v8.5' into v8.6
Pierre-Marie Pédrot
2016-08-24
CLEANUP: minor readability improvements
Matej Kosik
2016-05-08
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-03-20
Moving Refine to its proper module.
Pierre-Marie Pédrot