diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-23 12:27:19 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-26 14:41:00 +0100 |
| commit | a1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 (patch) | |
| tree | 108cd9d4644f9b610a6800eac6324d54455d1ec6 /pretyping/pretyping.mllib | |
| parent | 35fc7d7281688b248c55d3a8c2ed24b1c3fef38c (diff) | |
Experimenting always forcing convertibility on strict implicit arguments
in tactic unification.
Diffstat (limited to 'pretyping/pretyping.mllib')
| -rw-r--r-- | pretyping/pretyping.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index b189360c0..2958b9e73 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -31,4 +31,5 @@ Detyping Indrec Cases Pretyping +Impargs Unification |