From ba360bdefa2d7e4200c94a37c5065019718c2691 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 6 Mar 2010 16:34:11 +0000 Subject: Fixes in rewrite and a Elimination/Case to Scheme: - disallow dynamic generation of [case] constructs through [find_scheme] during a rewrite, as it changes the global environment and subsequent manipulations of the tactic may use an outdated environment. - use local exception names so as not to catch and hide unexpected [Not_found] exceptions. - fix lifting of constraints for dependent function types - Allow rewriting on morphisms (terms in function position) even with [rewrite] (fixes bug #2178). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12848 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/indschemes.ml | 66 ++++++++++++++++++++++++++------------------------ 1 file changed, 35 insertions(+), 31 deletions(-) (limited to 'toplevel/indschemes.ml') diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 1cd00068b..03a3ecac4 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -280,6 +280,7 @@ let rec split_scheme l = | (Some id,t)::q -> let l1,l2 = split_scheme q in ( match t with | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 + | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2 | EqualityScheme x -> l1,((Some id,smart_global_inductive x)::l2) ) (* @@ -287,38 +288,41 @@ let rec split_scheme l = requested *) | (None,t)::q -> - let l1,l2 = split_scheme q in - ( match t with - | InductionScheme (x,y,z) -> - let ind = smart_global_inductive y in - let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in - let z' = family_of_sort (interp_sort z) in - let suffix = ( - match sort_of_ind with - | InProp -> - if x then (match z' with - | InProp -> "_ind_nodep" - | InSet -> "_rec_nodep" - | InType -> "_rect_nodep") - else ( match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - | _ -> - if x then (match z' with - | InProp -> "_ind" - | InSet -> "_rec" - | InType -> "_rect" ) - else (match z' with - | InProp -> "_ind_dep" - | InSet -> "_rec_dep" - | InType -> "_rect_dep") - ) in - let newid = add_suffix (basename_of_global (IndRef ind)) suffix in - let newref = (dummy_loc,newid) in + let l1,l2 = split_scheme q in + let names inds recs x y z = + let ind = smart_global_inductive y in + let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in + let z' = family_of_sort (interp_sort z) in + let suffix = ( + match sort_of_ind with + | InProp -> + if x then (match z' with + | InProp -> inds ^ "_nodep" + | InSet -> recs ^ "_nodep" + | InType -> recs ^ "t_nodep") + else ( match z' with + | InProp -> inds + | InSet -> recs + | InType -> recs ^ "t" ) + | _ -> + if x then (match z' with + | InProp -> inds + | InSet -> recs + | InType -> recs ^ "t" ) + else (match z' with + | InProp -> inds ^ "_dep" + | InSet -> recs ^ "_dep" + | InType -> recs ^ "t_dep") + ) in + let newid = add_suffix (basename_of_global (IndRef ind)) suffix in + let newref = (dummy_loc,newid) in ((newref,x,ind,z)::l1),l2 - | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) - ) + in + match t with + | CaseScheme (x,y,z) -> names "_case" "_case" x y z + | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z + | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) + let do_mutual_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort -- cgit v1.2.3