diff options
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | interp/interp.mllib | 1 | ||||
-rw-r--r-- | library/impargs.ml | 84 | ||||
-rw-r--r-- | library/impargs.mli | 2 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
-rw-r--r-- | pretyping/unification.ml | 109 | ||||
-rw-r--r-- | tactics/equality.ml | 16 |
7 files changed, 84 insertions, 130 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index ec362b538..2e61cb697 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -144,7 +144,6 @@ Program Coercion Cases Pretyping -Impargs Unification Declaremods Library diff --git a/interp/interp.mllib b/interp/interp.mllib index d3b7077c4..c9a031526 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -10,6 +10,7 @@ Dumpglob Syntax_def Smartlocate Reserve +Impargs Implicit_quantifiers Constrintern Modintern diff --git a/library/impargs.ml b/library/impargs.ml index e3c5c84b0..d88d6f106 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -268,9 +268,6 @@ let compute_implicits_names env t = let _, impls = compute_implicits_gen false false false false true env t in List.map fst impls -let compute_implicits_strict env t = - List.map snd (snd (compute_implicits_gen true true true true false env t)) - (* Extra information about implicit arguments *) type maximal_insertion = bool (* true = maximal contextual insertion *) @@ -396,16 +393,14 @@ let set_manual_implicits env flags enriching autoimps l = merge 1 l autoimps let compute_semi_auto_implicits env f manual t = - let strictimpls = compute_implicits_strict env t in - let auto = match manual with + match manual with | [] -> if not f.auto then [DefaultImpArgs, []] else let _,l = compute_implicits_flags env f false t in [DefaultImpArgs, prepare_implicits f l] | _ -> let _,autoimpls = compute_auto_implicits env f f.auto t in - [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] in - strictimpls,auto + [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual] (*s Constants. *) @@ -488,21 +483,9 @@ type implicit_discharge_request = let implicits_table = Summary.ref Refmap.empty ~name:"implicits" -let strict_implicits_of_global n ref = - try - let impls = fst (Refmap.find ref !implicits_table) in - let status = List.map (function - | Some (DepRigid (Hyp k) | DepFlexAndRigid (_,Hyp k)) -> k <= n - | _ -> false) impls in - let m = List.length status in - if m > n then fst (List.chop n status) - else if m < n then status @ List.make (n-m) false - else status - with Not_found -> anomaly (str "No strict implicit arguments." ++ Nametab.pr_global_env Idset.empty ref) - let implicits_of_global ref = try - let l = snd (Refmap.find ref !implicits_table) in + let l = Refmap.find ref !implicits_table in try let rename_l = Arguments_renaming.arguments_names ref in let rename imp name = match imp, name with @@ -530,14 +513,14 @@ let subst_implicits (subst,(req,l)) = let impls_of_context ctx = let map (id, impl, _, _) = match impl with - | Implicit -> Some (* dummy *) Manual, Some (id, Manual, (true, true)) - | _ -> None, None + | Implicit -> Some (id, Manual, (true, true)) + | _ -> None in let is_set (_, _, b, _) = match b with | None -> true | Some _ -> false in - List.split (List.rev_map map (List.filter is_set ctx)) + List.rev_map map (List.filter is_set ctx) let section_segment_of_reference = function | ConstRef con -> pi1 (section_segment_of_constant con) @@ -560,33 +543,26 @@ let discharge_implicits (_,(req,l)) = (try let vars = section_segment_of_reference ref in let ref' = if isVarRef ref then ref else pop_global_reference ref in - let extrastrict, extra_impls = impls_of_context vars in - let oldstrict,oldimpls = snd (List.hd l) in - let newstrict = extrastrict @ oldstrict in - let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in - let l' = [ref',(newstrict,newimpls)] in + let extra_impls = impls_of_context vars in + let l' = [ref', List.map (add_section_impls vars extra_impls) (snd (List.hd l))] in Some (ImplInteractive (ref',flags,exp),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) | ImplConstant (con,flags) -> (try let con' = pop_con con in let vars,_,_ = section_segment_of_constant con in - let extrastrict, extra_impls = impls_of_context vars in - let oldstrict,oldimpls = snd (List.hd l) in - let newstrict = extrastrict @ oldstrict in - let newimpls = List.map (add_section_impls vars extra_impls) oldimpls in - let l' = [ConstRef con',(newstrict,newimpls)] in + let extra_impls = impls_of_context vars in + let newimpls = List.map (add_section_impls vars extra_impls) (snd (List.hd l)) in + let l' = [ConstRef con',newimpls] in Some (ImplConstant (con',flags),l') with Not_found -> (* con not defined in this section *) Some (req,l)) | ImplMutualInductive (kn,flags) -> (try - let l' = List.map (fun (gr, (newstrict,l)) -> + let l' = List.map (fun (gr, l) -> let vars = section_segment_of_reference gr in - let extrastrict, extra_impls = impls_of_context vars in - let newstrict = extrastrict @ newstrict in - let newimpls = List.map (add_section_impls vars extra_impls) l in + let extra_impls = impls_of_context vars in ((if isVarRef gr then gr else pop_global_reference gr), - (newstrict,newimpls))) l + List.map (add_section_impls vars extra_impls) l)) l in Some (ImplMutualInductive (pop_kn kn,flags),l') with Not_found -> (* ref not defined in this section *) Some (req,l)) @@ -595,16 +571,15 @@ let rebuild_implicits (req,l) = match req with | ImplLocal -> assert false | ImplConstant (con,flags) -> - let _,oldimpls = snd (List.hd l) in - let newstrict,newimpls = compute_constant_implicits flags [] con in - req, [ConstRef con, (newstrict,List.map2 merge_impls oldimpls newimpls)] + let oldimpls = snd (List.hd l) in + let newimpls = compute_constant_implicits flags [] con in + req, [ConstRef con, List.map2 merge_impls oldimpls newimpls] | ImplMutualInductive (kn,flags) -> let newimpls = compute_all_mib_implicits flags [] kn in let rec aux olds news = match olds, news with - | (_, (_,oldimpls)) :: old, (gr, (newstrict,newimpls)) :: tl -> - (gr, (newstrict,List.map2 merge_impls oldimpls newimpls)) - :: aux old tl + | (_, oldimpls) :: old, (gr, newimpls) :: tl -> + (gr, List.map2 merge_impls oldimpls newimpls) :: aux old tl | [], [] -> [] | _, _ -> assert false in req, aux l newimpls @@ -613,19 +588,18 @@ let rebuild_implicits (req,l) = (if isVarRef ref && is_in_section ref then ImplLocal else req), match o with | ImplAuto -> - let _,oldimpls = snd (List.hd l) in - let newstrict,newimpls = compute_global_implicits flags [] ref in - [ref,(newstrict,List.map2 merge_impls oldimpls newimpls)] + let oldimpls = snd (List.hd l) in + let newimpls = compute_global_implicits flags [] ref in + [ref,List.map2 merge_impls oldimpls newimpls] | ImplManual userimplsize -> - let _,oldimpls = snd (List.hd l) in - let newstrict,newimpls = compute_global_implicits flags [] ref in - let newimpls = List.hd newimpls in + let oldimpls = snd (List.hd l) in if flags.auto then + let newimpls = List.hd (compute_global_implicits flags [] ref) in let p = List.length (snd newimpls) - userimplsize in let newimpls = on_snd (List.firstn p) newimpls in - [ref,(newstrict,List.map (fun o -> merge_impls o newimpls) oldimpls)] + [ref,List.map (fun o -> merge_impls o newimpls) oldimpls] else - [ref,(newstrict,oldimpls)] + [ref,oldimpls] let classify_implicits (req,_ as obj) = match req with | ImplLocal -> Dispose @@ -633,8 +607,7 @@ let classify_implicits (req,_ as obj) = match req with type implicits_obj = implicit_discharge_request * - (global_reference * - (implicit_explanation option list * implicits_list list)) list + (global_reference * implicits_list list) list let inImplicits : implicits_obj -> obj = declare_object {(default_object "IMPLICITS") with @@ -719,12 +692,11 @@ let declare_manual_implicits local ref ?enriching l = List.map (fun (imps,n) -> (LessArgsThan (nargs-n), set_manual_implicits env flags enriching autoimpls imps)) l in - let strictimpls = compute_implicits_strict env t in let req = if is_local local ref then ImplLocal else ImplInteractive(ref,flags,ImplManual (List.length autoimpls)) in - add_anonymous_leaf (inImplicits (req,[ref,(strictimpls,l')])) + add_anonymous_leaf (inImplicits (req,[ref,l'])) let maybe_declare_manual_implicits local ref ?enriching l = match l with diff --git a/library/impargs.mli b/library/impargs.mli index 3ba928508..297145f09 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -120,8 +120,6 @@ val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool val implicits_of_global : global_reference -> implicits_list list -val strict_implicits_of_global : int -> global_reference -> bool list - val extract_impargs_data : implicits_list list -> ((int * int) option * implicit_status list) list diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 2958b9e73..b189360c0 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -31,5 +31,4 @@ Detyping Indrec Cases Pretyping -Impargs Unification diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fa419ddaf..8009bad2d 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -592,7 +592,7 @@ let eta_constructor_app env f l1 term = | _ -> assert false let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = - let rec unirec_rec (curenv,nb as curenvnb) pb opt flags ((sigma,metasubst,evarsubst) as substn) curm curn = + let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm and cN = Evarutil.whd_head_evar sigma curn in let () = @@ -678,28 +678,28 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb error_cannot_unify curenv sigma (m,n)) | Lambda (na,t1,c1), Lambda (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} flags - (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} flags substn t1 t2) c1 c2 + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} + (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 | Prod (na,t1,c1), Prod (_,t2,c2) -> - unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} flags - (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} flags substn t1 t2) c1 c2 - | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt flags substn (subst1 a c) cN - | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt flags substn cM (subst1 a c) + unirec_rec (push (na,t1) curenvnb) pb {opt with at_top = true} + (unirec_rec curenvnb CONV {opt with at_top = true; with_types = false} substn t1 t2) c1 c2 + | LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb opt substn (subst1 a c) cN + | _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb opt substn cM (subst1 a c) (** Fast path for projections. *) | Proj (p1,c1), Proj (p2,c2) when eq_constant (Projection.constant p1) (Projection.constant p2) -> - (try unify_same_proj curenvnb cv_pb {opt with at_top = true} flags + (try unify_same_proj curenvnb cv_pb {opt with at_top = true} substn c1 c2 with ex when precatchable_exception ex -> - unify_not_same_head curenvnb pb opt flags substn cM cN) + unify_not_same_head curenvnb pb opt substn cM cN) (* eta-expansion *) | Lambda (na,t1,c1), _ when flags.modulo_eta -> - unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} flags substn + unirec_rec (push (na,t1) curenvnb) CONV {opt with at_top = true} substn c1 (mkApp (lift 1 cN,[|mkRel 1|])) | _, Lambda (na,t2,c2) when flags.modulo_eta -> - unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} flags substn + unirec_rec (push (na,t2) curenvnb) CONV {opt with at_top = true} substn (mkApp (lift 1 cM,[|mkRel 1|])) c2 (* For records *) @@ -710,7 +710,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (try let l1', l2' = eta_constructor_app curenv f1 l1 cN in let opt' = {opt with at_top = true; with_cs = false} in - Array.fold_left2 (unirec_rec curenvnb CONV opt' flags) substn l1' l2' + Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' with ex when precatchable_exception ex -> match kind_of_term cN with | App(f2,l2) when isMeta f2 || isEvar f2 -> @@ -722,7 +722,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (try let l2', l1' = eta_constructor_app curenv f2 l2 cM in let opt' = {opt with at_top = true; with_cs = false} in - Array.fold_left2 (unirec_rec curenvnb CONV opt' flags) substn l1' l2' + Array.fold_left2 (unirec_rec curenvnb CONV opt') substn l1' l2' with ex when precatchable_exception ex -> match kind_of_term cM with | App(f1,l1) when isMeta f1 || isEvar f1 -> @@ -732,12 +732,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Case (_,p1,c1,cl1), Case (_,p2,c2,cl2) -> (try let opt' = {opt with at_top = true; with_types = false} in - Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true} flags) - (unirec_rec curenvnb CONV opt' flags - (unirec_rec curenvnb CONV opt' flags substn p1 p2) c1 c2) + Array.fold_left2 (unirec_rec curenvnb CONV {opt with at_top = true}) + (unirec_rec curenvnb CONV opt' + (unirec_rec curenvnb CONV opt' substn p1 p2) c1 c2) cl1 cl2 with ex when precatchable_exception ex -> - reduce curenvnb pb opt flags substn cM cN) + reduce curenvnb pb opt substn cM cN) | App (f1,l1), _ when (isMeta f1 && use_metas_pattern_unification flags nb l1 @@ -749,7 +749,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (match kind_of_term cN with | App (f2,l2) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 | Proj _ -> unify_app curenvnb pb opt substn cM f1 l1 cN cN [||] - | _ -> unify_not_same_head curenvnb pb opt flags substn cM cN) + | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f1 l cN substn) @@ -763,7 +763,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb (match kind_of_term cM with | App (f1,l1) -> unify_app curenvnb pb opt substn cM f1 l1 cN f2 l2 | Proj _ -> unify_app curenvnb pb opt substn cM cM [||] cN f2 l2 - | _ -> unify_not_same_head curenvnb pb opt flags substn cM cN) + | _ -> unify_not_same_head curenvnb pb opt substn cM cN) | Some l -> solve_pattern_eqn_array curenvnb f2 l cM substn) @@ -777,7 +777,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb unify_app curenvnb pb opt substn cM cM [||] cN f2 l2 | _ -> - unify_not_same_head curenvnb pb opt flags substn cM cN + unify_not_same_head curenvnb pb opt substn cM cN and unify_app (curenv, nb as curenvnb) pb opt (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 = try @@ -801,32 +801,20 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let f2, l2 = expand_proj f2 f1 l2 in let opta = {opt with at_top = true; with_types = false} in let optf = {opt with at_top = true; with_types = true} in - let same_glob f1 f2 = - try Globnames.RefOrdered.equal (Globnames.global_of_constr f1) (Globnames.global_of_constr f2) && not (isVar f1) - with Not_found -> false in - if same_glob f1 f2 && Int.equal (Array.length l1) (Array.length l2) then - let impls = - Impargs.strict_implicits_of_global (Array.length l1) (Globnames.global_of_constr f1) in - Array.fold_left3 - (fun subst b -> unirec_rec curenvnb CONV optf - (if b then default_core_unify_flags () else flags) subst) - (unirec_rec curenvnb CONV optf flags substn f1 f2) - (Array.of_list impls) l1 l2 - else let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in if Array.length l1 == 0 then error_cannot_unify (fst curenvnb) sigma (cM,cN) else - Array.fold_left2 (unirec_rec curenvnb CONV opta flags) - (unirec_rec curenvnb CONV optf flags substn f1 f2) l1 l2 + Array.fold_left2 (unirec_rec curenvnb CONV opta) + (unirec_rec curenvnb CONV optf substn f1 f2) l1 l2 with ex when precatchable_exception ex -> - try reduce curenvnb pb {opt with with_types = false} flags substn cM cN + try reduce curenvnb pb {opt with with_types = false} substn cM cN with ex when precatchable_exception ex -> - try canonical_projections curenvnb pb opt flags cM cN substn + try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> - expand curenvnb pb {opt with with_types = false} flags substn cM f1 l1 cN f2 l2 + expand curenvnb pb {opt with with_types = false} substn cM f1 l1 cN f2 l2 - and unify_same_proj (curenv, nb as curenvnb) cv_pb opt flags substn c1 c2 = - let substn = unirec_rec curenvnb CONV opt flags substn c1 c2 in + and unify_same_proj (curenv, nb as curenvnb) cv_pb opt substn c1 c2 = + let substn = unirec_rec curenvnb CONV opt substn c1 c2 in try (* Force unification of the types to fill in parameters *) let ty1 = get_type_of curenv ~lax:true sigma c1 in let ty2 = get_type_of curenv ~lax:true sigma c2 in @@ -838,33 +826,33 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb ty1 ty2 with RetypeError _ -> substn - and unify_not_same_head curenvnb pb opt flags (sigma, metas, evars as substn) cM cN = - try canonical_projections curenvnb pb opt flags cM cN substn + and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn) cM cN = + try canonical_projections curenvnb pb opt cM cN substn with ex when precatchable_exception ex -> let sigma', b = constr_cmp cv_pb sigma flags cM cN in if b then (sigma', metas, evars) else - try reduce curenvnb pb opt flags substn cM cN + try reduce curenvnb pb opt substn cM cN with ex when precatchable_exception ex -> let (f1,l1) = match kind_of_term cM with App (f,l) -> (f,l) | _ -> (cM,[||]) in let (f2,l2) = match kind_of_term cN with App (f,l) -> (f,l) | _ -> (cN,[||]) in - expand curenvnb pb opt flags substn cM f1 l1 cN f2 l2 + expand curenvnb pb opt substn cM f1 l1 cN f2 l2 - and reduce curenvnb pb opt flags (sigma, metas, evars as substn) cM cN = + and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN = if use_full_betaiota flags && not (subterm_restriction opt flags) then let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in if not (Term.eq_constr cM cM') then - unirec_rec curenvnb pb opt flags substn cM' cN + unirec_rec curenvnb pb opt substn cM' cN else let cN' = do_reduce flags.modulo_delta curenvnb sigma cN in if not (Term.eq_constr cN cN') then - unirec_rec curenvnb pb opt flags substn cM cN' + unirec_rec curenvnb pb opt substn cM cN' else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and expand (curenv,_ as curenvnb) pb opt flags (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 = + and expand (curenv,_ as curenvnb) pb opt (sigma,metasubst,evarsubst as substn) cM f1 l1 cN f2 l2 = let res = (* Try full conversion on meta-free terms. *) (* Back to 1995 (later on called trivial_unify in 2002), the @@ -906,35 +894,35 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb | Some true -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> - unirec_rec curenvnb pb opt flags substn + unirec_rec curenvnb pb opt substn (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> - unirec_rec curenvnb pb opt flags substn cM + unirec_rec curenvnb pb opt substn cM (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> error_cannot_unify curenv sigma (cM,cN))) | Some false -> (match expand_key flags.modulo_delta curenv sigma cf2 with | Some c -> - unirec_rec curenvnb pb opt flags substn cM + unirec_rec curenvnb pb opt substn cM (whd_betaiotazeta sigma (mkApp(c,l2))) | None -> (match expand_key flags.modulo_delta curenv sigma cf1 with | Some c -> - unirec_rec curenvnb pb opt flags substn + unirec_rec curenvnb pb opt substn (whd_betaiotazeta sigma (mkApp(c,l1))) cN | None -> error_cannot_unify curenv sigma (cM,cN))) - and canonical_projections (curenv, _ as curenvnb) pb opt flags cM cN (sigma,_,_ as substn) = + and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) = let f1 () = if isApp cM then let f1l1 = whd_nored_state sigma (cM,Stack.empty) in if is_open_canonical_projection curenv sigma f1l1 then let f2l2 = whd_nored_state sigma (cN,Stack.empty) in - solve_canonical_projection curenvnb pb opt flags cM f1l1 cN f2l2 substn + solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) in @@ -950,11 +938,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb let f2l2 = whd_nored_state sigma (cN, Stack.empty) in if is_open_canonical_projection curenv sigma f2l2 then let f1l1 = whd_nored_state sigma (cM, Stack.empty) in - solve_canonical_projection curenvnb pb opt flags cN f2l2 cM f1l1 substn + solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn else error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) - and solve_canonical_projection curenvnb pb opt flags cM f1l1 cN f2l2 (sigma,ms,es) = + and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) = let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) = try Evarconv.check_conv_record f1l1 f2l2 with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -973,15 +961,15 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb try let opt' = {opt with with_types = false} in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb opt' flags s u1 (substl ks u)) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) (evd,ms,es) us2 us in let (substn,_,_) = Reductionops.Stack.fold2 - (fun s u1 u -> unirec_rec curenvnb pb opt' flags s u1 (substl ks u)) + (fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u)) substn params1 params in - let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt' flags ) substn ts ts1 in + let (substn,_,_) = Reductionops.Stack.fold2 (unirec_rec curenvnb pb opt') substn ts ts1 in let app = mkApp (c, Array.rev_of_list ks) in (* let substn = unirec_rec curenvnb pb b false substn t cN in *) - unirec_rec curenvnb pb opt' flags substn c1 app + unirec_rec curenvnb pb opt' substn c1 app with Invalid_argument "Reductionops.Stack.fold2" -> error_cannot_unify (fst curenvnb) sigma (cM,cN) else error_cannot_unify (fst curenvnb) sigma (cM,cN) @@ -1007,8 +995,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb try let a = match res with | Some sigma -> sigma, ms, es - | None -> unirec_rec (env,0) cv_pb opt flags subst m n - in + | None -> unirec_rec (env,0) cv_pb opt subst m n in if !debug_unification then msg_debug (str "Leaving unification with success"); a with e -> diff --git a/tactics/equality.ml b/tactics/equality.ml index a7fc38a23..d6083860a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -170,9 +170,8 @@ let instantiate_lemma gl c ty l l2r concl = let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in [eqclause] -let rewrite_conv_closed_core_unif_flags env = - let ts = Conv_oracle.get_transp_state (Environ.oracle env) in { - modulo_conv_on_closed_terms = Some ts; +let rewrite_conv_closed_core_unif_flags = { + modulo_conv_on_closed_terms = Some full_transparent_state; (* We have this flag for historical reasons, it has e.g. the consequence *) (* to rewrite "?x+2" in "y+(1+1)=0" or to rewrite "?x+?x" in "2+(1+1)=0" *) @@ -198,18 +197,17 @@ let rewrite_conv_closed_core_unif_flags env = modulo_eta = true; } -let rewrite_conv_closed_unif_flags env = - let flags = rewrite_conv_closed_core_unif_flags env in { - core_unify_flags = flags; - merge_unify_flags = flags; - subterm_unify_flags = flags; +let rewrite_conv_closed_unif_flags = { + core_unify_flags = rewrite_conv_closed_core_unif_flags; + merge_unify_flags = rewrite_conv_closed_core_unif_flags; + subterm_unify_flags = rewrite_conv_closed_core_unif_flags; allow_K_in_toplevel_higher_order_unification = false; resolve_evars = false } let rewrite_elim with_evars frzevars cls c e = Proofview.Goal.enter begin fun gl -> - let flags = make_flags frzevars (Proofview.Goal.sigma gl) (rewrite_conv_closed_unif_flags (Proofview.Goal.env gl)) c in + let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in general_elim_clause with_evars flags cls c e end |