diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 7 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 7 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 4 |
3 files changed, 7 insertions, 11 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 94d3c1b69..bdd1a8ba1 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -67,12 +67,11 @@ let applyHead n c wc = else match kind_of_term (w_whd_betadeltaiota wc cty) with | IsProd (_,c1,c2) -> - let c1ty = w_type_of wc c1 in let evar = Evarutil.new_evar_in_sign (w_env wc) in let (evar_n, _) = destEvar evar in (compose (apprec (n-1) (applist(c,[evar])) (subst1 evar c2)) - (w_Declare evar_n (c1,c1ty))) + (w_Declare evar_n c1)) wc | _ -> error "Apply_Head_Then" in @@ -946,9 +945,7 @@ let clenv_pose_dependent_evars clenv = let evar = Evarutil.new_evar_in_sign (w_env clenv.hook) in let (evar_n,_) = destEvar evar in let tY = clenv_instance_type clenv mv in - let tYty = w_type_of clenv.hook tY in - let clenv' = clenv_wtactic (w_Declare evar_n (tY,tYty)) - clenv in + let clenv' = clenv_wtactic (w_Declare evar_n tY) clenv in clenv_assign mv evar clenv') clenv dep_mvs diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index f99608691..9e9d6c8fb 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -133,12 +133,11 @@ let w_whd_betadeltaiota wc c = whd_betadeltaiota (w_env wc) (w_Underlying wc) c let w_hnf_constr wc c = hnf_constr (w_env wc) (w_Underlying wc) c -let w_Declare sp (ty,s) (wc : walking_constraints) = - let c = mkCast (ty,s) in - let _ = w_type_of wc c in +let w_Declare sp ty (wc : walking_constraints) = + let _ = w_type_of wc ty in (* Utile ?? *) let access = get_focus (ids_it wc) and sign = get_hyps (ids_it wc) in - let newdecl = mk_goal (mt_ctxt access) sign c in + let newdecl = mk_goal (mt_ctxt access) sign ty in ((ids_mod (fun evc -> (rc_add evc (sp,newdecl))) wc): walking_constraints) let w_Declare_At sp sp' c = w_Focusing sp (w_Declare sp' c) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index b5af7f131..88071b3af 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -52,8 +52,8 @@ val walking : w_tactic -> tactic val w_Focusing_THEN : evar -> 'a result_w_tactic -> ('a -> w_tactic) -> w_tactic -val w_Declare : evar -> constr * constr -> w_tactic -val w_Declare_At : evar -> evar -> constr * constr -> w_tactic +val w_Declare : evar -> types -> w_tactic +val w_Declare_At : evar -> evar -> types -> w_tactic val w_Define : evar -> constr -> w_tactic val w_Underlying : walking_constraints -> enamed_declarations |