From 954fbd3b102060ed1e2122f571a430f05a174e42 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 9 May 2017 22:14:35 +0200 Subject: Remove the Sigma (monotonous state) API. Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good. --- vernac/auto_ind_decl.ml | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) (limited to 'vernac/auto_ind_decl.ml') 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 -- cgit v1.2.3