aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comDefinition.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-04 15:54:28 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-31 18:44:19 +0200
commit9f723f14e5342c1303646b5ea7bb5c0012a090ef (patch)
treed6a6a82ab8b73e975588a547eb15a5a2f83fd4c7 /vernac/comDefinition.ml
parent2d2d16430822f1768ce4f3c62ef0750b94e4747f (diff)
[econstr] Forbid calling `to_constr` in open terms.
We forbid calling `EConstr.to_constr` on terms that are not evar-free, as to progress towards enforcing the invariant that `Constr.t` is evar-free. [c.f. #6308] Due to compatibility constraints we provide an optional parameter to `to_constr`, `abort` which can be used to overcome this restriction until we fix all parts of the code. Now, grepping for `~abort:false` should return the questionable parts of the system. Not a lot of places had to be fixed, some comments: - problems with the interface due to `Evd/Constr` [`Evd.define` being the prime example] do seem real! - inductives also look bad with regards to `Constr/EConstr`. - code in plugins needs work. A notable user of this "feature" is `Obligations/Program` that seem to like to generate kernel-level entries with free evars, then to scan them and workaround this problem by generating constants.
Diffstat (limited to 'vernac/comDefinition.ml')
-rw-r--r--vernac/comDefinition.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b18a60a1f..9aa61ab46 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt =
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
Note: in program mode some evars may remain. *)
- let ctx = List.map (EConstr.to_rel_decl evd) ctx in
- let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
+ 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
(* Keep only useful universes. *)
let uvars_fold uvars c =