diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 40 | ||||
| -rw-r--r-- | vernac/classes.ml | 3 | ||||
| -rw-r--r-- | vernac/command.ml | 9 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 9 | ||||
| -rw-r--r-- | vernac/record.ml | 9 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
6 files changed, 29 insertions, 45 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index b99ccbf4a..9e6e5e313 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -365,7 +365,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ))) ) in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let type_of_pq = Tacmach.New.pf_unsafe_type_of gl p in let sigma = Tacmach.New.project gl in let u,v = destruct_ind sigma type_of_pq @@ -397,7 +397,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = Tacticals.New.tclTHENLIST [ Proofview.tclEFFECTS eff; Equality.replace p q ; apply app ; Auto.default_auto] - end } + end (* used in the bool -> leib side *) let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = @@ -430,7 +430,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in let sigma = Tacmach.New.project gl in if EConstr.eq_constr sigma t1 t2 then aux q1 q2 @@ -472,7 +472,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = aux q1 q2 ] ) ) - end } + end | ([],[]) -> Proofview.tclUNIT () | _ -> Tacticals.New.tclZEROMSG (str "Both side of the equality must have the same arity.") in @@ -581,7 +581,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -604,18 +604,18 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [ Simple.apply_in freshz (EConstr.of_constr (andb_prop())); - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in destruct_on_as (EConstr.mkVar freshz) (IntroOrPattern [[Loc.tag @@ IntroNaming (IntroIdentifier fresht); Loc.tag @@ IntroNaming (IntroIdentifier freshz)]]) - end } + end ]); (* Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in match EConstr.kind sigma concl with @@ -635,10 +635,10 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.") ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.") - end } + end ] - end } + end let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined") @@ -725,7 +725,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -748,7 +748,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro())); simplest_split ;Auto.default_auto ] ); - Proofview.Goal.enter { enter = begin fun gls -> + Proofview.Goal.enter begin fun gls -> let concl = Proofview.Goal.concl gls in let sigma = Tacmach.New.project gl in (* assume the goal to be eq (eq_type ...) = true *) @@ -765,9 +765,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = ) | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.") - end } + end ] - end } + end let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined") @@ -873,7 +873,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let fresh = fresh_id_in_env (!avoid) s (Proofview.Goal.env gl) in avoid := fresh::(!avoid); fresh in - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in let freshn = fresh_id (Id.of_string "x") gl in let freshm = fresh_id (Id.of_string "y") gl in @@ -904,7 +904,7 @@ let compute_dec_tact ind lnamesparrec nparrec = )) (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto); - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let freshH2 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [ (* left *) @@ -916,7 +916,7 @@ let compute_dec_tact ind lnamesparrec nparrec = ; (*right *) - Proofview.Goal.enter { enter = begin fun gl -> + Proofview.Goal.enter begin fun gl -> let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; @@ -938,11 +938,11 @@ let compute_dec_tact ind lnamesparrec nparrec = true; Equality.discr_tac false None ] - end } + end ] - end } + end ] - end } + end let make_eq_decidability mode mind = let mib = Global.lookup_mind mind in diff --git a/vernac/classes.ml b/vernac/classes.ml index 004083dcf..dc5ce1a53 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -20,7 +20,6 @@ open Libnames open Globnames open Constrintern open Constrexpr -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -342,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine { run = fun evm -> Sigma (EConstr.of_constr (Option.get term), evm, Sigma.refl) }; + Refine.refine (fun evm -> (evm,EConstr.of_constr (Option.get term))); Proofview.Unsafe.tclNEWGOALS gls; Tactics.New.reduce_after_refine; ] diff --git a/vernac/command.ml b/vernac/command.ml index ad84c17b7..b1425d703 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -35,7 +35,6 @@ open Evarconv open Indschemes open Misctypes open Vernacexpr -open Sigma.Notations open Context.Rel.Declaration open Entries @@ -78,8 +77,7 @@ let red_constant_entry n ce sigma = function let env = Global.env () in let (redfun, _) = reduction_of_red_expr env red in let redfun env sigma c = - let sigma = Sigma.Unsafe.of_evar_map sigma in - let Sigma (c, _, _) = redfun.e_redfun env sigma c in + let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in { ce with const_entry_body = Future.chain ~pure:true proof_out @@ -908,9 +906,8 @@ let tactics_module = subtac_dir @ ["Tactics"] let init_reference dir s () = Coqlib.coq_reference "Command" dir s let init_constant dir s evdref = - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map !evdref) - (Coqlib.coq_reference "Command" dir s) - in evdref := Sigma.to_evar_map sigma; c + let (sigma, c) = Evarutil.new_global !evdref (Coqlib.coq_reference "Command" dir s) + in evdref := sigma; c let make_ref l s = init_reference l s let fix_proto = init_constant tactics_module "fix_proto" diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index a678d20bb..c2c27eb78 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -453,13 +453,8 @@ let fold_left' f = function [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl -let new_global sigma gr = - let open Sigma in - let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr - in Sigma.to_evar_map sigma, c - -let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ()) -let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ()) +let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) +let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in diff --git a/vernac/record.ml b/vernac/record.ml index 8cde88dc9..2400fa681 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -24,7 +24,6 @@ open Type_errors open Constrexpr open Constrexpr_ops open Goptions -open Sigma.Notations open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -365,15 +364,11 @@ let structure_signature ctx = match l with [] -> Evd.empty | [decl] -> let env = Environ.empty_named_context_val in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (_, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - let evm = Sigma.to_evar_map evm in + let (evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in evm | decl::tl -> let env = Environ.empty_named_context_val in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (ev, evm, _) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in - let evm = Sigma.to_evar_map evm in + let (evm, ev) = Evarutil.new_pure_evar env evm (EConstr.of_constr (RelDecl.get_type decl)) in let new_tl = Util.List.map_i (fun pos decl -> RelDecl.map_type (fun t -> EConstr.Unsafe.to_constr (Termops.replace_term evm (EConstr.mkRel pos) (EConstr.mkEvar(ev,[||])) (EConstr.of_constr t))) decl) 1 tl in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c6ec89c5e..1332a7052 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -31,7 +31,6 @@ open Redexpr open Lemmas open Misctypes open Locality -open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -1550,8 +1549,7 @@ let vernac_check_may_eval ?loc redexp glopt rc = let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in - let evm = Sigma.Unsafe.of_evar_map evm in - let Sigma (c, _, _) = redfun.Reductionops.e_redfun env evm c in + let (_, c) = redfun env evm c in c in Feedback.msg_notice (print_eval redfun env sigma' rc j) |