diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 20 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 |
2 files changed, 16 insertions, 8 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d01338fa95..b7ccd647b5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -603,12 +603,20 @@ let make_evar_clause env sigma ?len t = in (** FIXME: do the renaming online *) let t = rename_bound_vars_as_displayed sigma Id.Set.empty [] t in - let rec clrec (sigma, holes) n t = + let rec clrec (sigma, holes) inst n t = if n = 0 then (sigma, holes, t) else match EConstr.kind sigma t with - | Cast (t, _, _) -> clrec (sigma, holes) n t + | Cast (t, _, _) -> clrec (sigma, holes) inst n t | Prod (na, t1, t2) -> - let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in + (** Share the evar instances as we are living in the same context *) + let inst, ctx, args, subst = match inst with + | None -> + (** Dummy type *) + let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in + Some (ctx, args, subst), ctx, args, subst + | Some (ctx, args, subst) -> inst, ctx, args, subst + in + let (sigma, ev) = new_evar_instance ~typeclass_candidate:false ctx sigma (csubst_subst subst t1) args in let dep = not (noccurn sigma 1 t2) in let hole = { hole_evar = ev; @@ -618,11 +626,11 @@ let make_evar_clause env sigma ?len t = hole_name = na; } in let t2 = if dep then subst1 ev t2 else t2 in - clrec (sigma, hole :: holes) (pred n) t2 - | LetIn (na, b, _, t) -> clrec (sigma, holes) n (subst1 b t) + clrec (sigma, hole :: holes) inst (pred n) t2 + | LetIn (na, b, _, t) -> clrec (sigma, holes) inst n (subst1 b t) | _ -> (sigma, holes, t) in - let (sigma, holes, t) = clrec (sigma, []) bound t in + let (sigma, holes, t) = clrec (sigma, []) None bound t in let holes = List.rev holes in let clause = { cl_concl = t; cl_holes = holes } in (sigma, clause) diff --git a/proofs/logic.ml b/proofs/logic.ml index b8612cd2c0..4d5711c195 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -384,7 +384,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) then + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let ty = (* Template polymorphism of definitions and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in @@ -447,7 +447,7 @@ and mk_hdgoals sigma goal goalacc trm = | App (f,l) -> let (acc',hdty,sigma,applicand) = - if is_template_polymorphic env sigma (EConstr.of_constr f) + if Termops.is_template_polymorphic_ind env sigma (EConstr.of_constr f) then let l' = meta_free_prefix sigma l in (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f) |