diff options
| author | Pierre-Marie Pédrot | 2014-03-01 16:16:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-01 16:16:14 +0100 |
| commit | da0db0a69a4e78841f9a8cf06ae4be17292bedbf (patch) | |
| tree | b54ed056c525e68e5bf880bbf208be196d0a71d8 | |
| parent | 124734fd2c523909802d095abb37350519856864 (diff) | |
Fixing bad comparison in Detyping.
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index c29c443b69..c591101241 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -684,7 +684,7 @@ let rec subst_glob_constr subst raw = | _ -> knd in let nsolve = Option.smartmap (Hook.get f_subst_genarg subst) solve in - if nsolve == solve && nknd = knd then raw + if nsolve == solve && nknd == knd then raw else GHole (loc, nknd, nsolve) | GCast (loc,r1,k) -> |