diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-26 21:25:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-11-26 21:25:39 +0100 |
| commit | 894a3d16471f19bd527730490ea242e218b62ff6 (patch) | |
| tree | f521ca6a51ae68f163dfbb637739d0f2efb7ad6b | |
| parent | a1a6d7b99eef5e6a671e5e6d057e46a6122e5e58 (diff) | |
Fixing Coq compilation.
| -rw-r--r-- | pretyping/unification.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0af61d3a2..fa419ddaf 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1008,6 +1008,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let a = match res with | Some sigma -> sigma, ms, es | None -> unirec_rec (env,0) cv_pb opt flags subst m n + in if !debug_unification then msg_debug (str "Leaving unification with success"); a with e -> |