diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 15:56:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-12 15:56:49 +0100 |
| commit | 1e5a7ded7b5ca5b2cca548f9a80ff8fd805e6ba1 (patch) | |
| tree | c1a9bf6a1a6289521840985743c5669da29087bf | |
| parent | c13476e65f9aa909d7fe8f0504ddc5f68e49b1f0 (diff) | |
Fixing compilation for 3.12.
| -rw-r--r-- | tactics/taccoerce.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index 74e2341bd..ab71f5f2e 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -177,6 +177,7 @@ let coerce_to_evaluable_ref env v = if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id else fail () else if has_type v (topwit wit_ref) then + let open Globnames in let r = out_gen (topwit wit_ref) v in match r with | VarRef var -> EvalVarRef var |