diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 16:55:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-05-17 16:55:19 +0200 |
| commit | 78c8d75e38844cb88c551881112e10728962dc2d (patch) | |
| tree | 742d6c1f6c914450427da2340b7a4f698afb6ea7 | |
| parent | 3229a681eaad0cbf4c2aec7d314d4baf0b96feaf (diff) | |
| parent | d10d62918f29ddaea773dd6b767b72ad0e038214 (diff) | |
Merge PR #7449: [vernac] taint two out-of-api `to_constr` use in `comDefinition`.
| -rw-r--r-- | vernac/comDefinition.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 9aa61ab46..863adb0d1 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -90,7 +90,7 @@ let interp_definition pl bl poly red_option c ctypopt = Note: in program mode some evars may remain. *) let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in - let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in + let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in (* Keep only useful universes. *) let uvars_fold uvars c = Univ.LSet.union uvars (universes_of_constr env evd (of_constr c)) @@ -118,7 +118,7 @@ let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook = assert(Univ.ContextSet.is_empty ctx); let typ = match ce.const_entry_type with | Some t -> t - | None -> EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) in Obligations.check_evars env evd; let obls, _, c, cty = |