diff options
Diffstat (limited to 'proofs/clenv.ml')
| -rw-r--r-- | proofs/clenv.ml | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 95e908c4dd..b7ccd647b5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function *) let clenv_pose_metas_as_evars clenv dep_mvs = - let rec fold clenv = function - | [] -> clenv + let rec fold clenv evs = function + | [] -> clenv, evs | mv::mvs -> let ty = clenv_meta_type clenv mv in (* Postpone the evar-ization if dependent on another meta *) (* This assumes no cycle in the dependencies - is it correct ? *) - if occur_meta clenv.evd ty then fold clenv (mvs@[mv]) + if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv]) else let src = evar_source_of_meta mv clenv.evd in let src = adjust_meta_source clenv.evd mv src in let evd = clenv.evd in let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in let clenv = clenv_assign mv evar {clenv with evd=evd} in - fold clenv mvs in - fold clenv dep_mvs + fold clenv (fst (destEvar evd evar) :: evs) mvs in + fold clenv [] dep_mvs (******************************************************************) @@ -577,7 +577,7 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ - pr_evar_map (Some 2) clenv.evd) + pr_evar_map (Some 2) clenv.env clenv.evd) (****************************************************************) (** Evar version of mk_clenv *) @@ -603,13 +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 store = Typeclasses.set_resolvable Evd.Store.empty false in - let (sigma, ev) = new_evar ~store env sigma 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; @@ -619,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) |