From 9f723f14e5342c1303646b5ea7bb5c0012a090ef Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 4 Dec 2017 15:54:28 +0100 Subject: [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. --- tactics/hints.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/hints.ml b/tactics/hints.ml index a285d6b93..46d162911 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -792,7 +792,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) = match EConstr.kind sigma cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in + let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -814,7 +814,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in + let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in -- cgit v1.2.3