diff options
author | 2014-11-23 12:27:19 +0100 | |
---|---|---|
committer | 2014-11-26 14:41:00 +0100 | |
commit | a1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 (patch) | |
tree | 108cd9d4644f9b610a6800eac6324d54455d1ec6 /interp | |
parent | 35fc7d7281688b248c55d3a8c2ed24b1c3fef38c (diff) |
Experimenting always forcing convertibility on strict implicit arguments
in tactic unification.
Diffstat (limited to 'interp')
-rw-r--r-- | interp/interp.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/interp.mllib b/interp/interp.mllib index c9a031526..d3b7077c4 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -10,7 +10,6 @@ Dumpglob Syntax_def Smartlocate Reserve -Impargs Implicit_quantifiers Constrintern Modintern |