diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 96 |
1 files changed, 48 insertions, 48 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index ebb6b165f..aea683dc6 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -217,7 +217,7 @@ let necessary_elimination sort_arity sort = Type_Type else errorlabstrm "necessary_elimination" - [< 'sTR "no primitive equality on proofs" >] + (str "no primitive equality on proofs") | _ -> if is_Set sort_arity then Set_SetorProp @@ -225,7 +225,7 @@ let necessary_elimination sort_arity sort = if is_Type sort_arity then Type_SetorProp else errorlabstrm "necessary_elimination" - [< 'sTR "no primitive equality on proofs" >] + (str "no primitive equality on proofs") let find_eq_pattern aritysort sort = match necessary_elimination aritysort sort with @@ -429,8 +429,8 @@ let construct_discriminator sigma env dirn c sort = CP : changed assert false in a more informative error *) errorlabstrm "Equality.construct_discriminator" - [< 'sTR "Cannot discriminate on inductive constructors with - dependent types" >] in + (str "Cannot discriminate on inductive constructors with + dependent types") in let (mib,mip) = lookup_mind_specif env ind in let arsign,arsort = get_arity env indf in let (true_0,false_0,sort_0) = @@ -473,7 +473,7 @@ let find_eq_data_decompose eqn = else if (is_matching (build_coq_idT_pattern ()) eqn) then (build_coq_idT_data, match_eq (build_coq_idT_pattern ()) eqn) else - errorlabstrm "find_eq_data_decompose" [< >] + errorlabstrm "find_eq_data_decompose" (mt ()) let gen_absurdity id gl = if is_empty_type (clause_type (Some id) gl) @@ -481,7 +481,7 @@ let gen_absurdity id gl = simplest_elim (mkVar id) gl else errorlabstrm "Equality.gen_absurdity" - [< 'sTR "Not the negation of an equality" >] + (str "Not the negation of an equality") (* Precondition: eq is leibniz equality @@ -529,14 +529,14 @@ let discr id gls = let (lbeq,(t,t1,t2)) = try find_eq_data_decompose eqn with e when catchable_exception e -> - errorlabstrm "discr" [<'sTR(string_of_id id); - 'sTR" Not a primitive equality here " >] + errorlabstrm "discr" (str(string_of_id id) ++ + str" Not a primitive equality here ") in let sigma = project gls in let env = pf_env gls in (match find_positions env sigma t1 t2 with | Inr _ -> - errorlabstrm "discr" [< 'sTR" Not a discriminable equality" >] + errorlabstrm "discr" (str" Not a discriminable equality") | Inl (cpath, (_,dirn), _) -> let e = pf_get_new_id (id_of_string "ee") gls in let e_env = push_named_decl (e,None,t) env in @@ -552,8 +552,8 @@ let discr id gls = let not_found_message id = - [<'sTR "The variable"; 'sPC ; 'sTR (string_of_id id) ; 'sPC; - 'sTR" was not found in the current environment" >] + (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++ + str" was not found in the current environment") let onNegatedEquality tac gls = if is_matching (build_coq_not_pattern ()) (pf_concl gls) then @@ -562,7 +562,7 @@ let onNegatedEquality tac gls = (tclTHEN intro (onLastHyp tac)) gls else errorlabstrm "extract_negated_equality_then" - [< 'sTR"The goal should negate an equality">] + (str"The goal should negate an equality") let discrClause = function | None -> onNegatedEquality discr @@ -572,7 +572,7 @@ let discrEverywhere = tclORELSE (Tacticals.tryAllClauses discrClause) (fun gls -> - errorlabstrm "DiscrEverywhere" [< 'sTR" No discriminable equalities" >]) + errorlabstrm "DiscrEverywhere" (str" No discriminable equalities")) let discrConcl gls = discrClause None gls let discrHyp id gls = discrClause (Some id) gls @@ -773,19 +773,19 @@ let inj id gls = try find_eq_data_decompose eqn with e when catchable_exception e -> - errorlabstrm "Inj" [<'sTR(string_of_id id); - 'sTR" Not a primitive equality here " >] + errorlabstrm "Inj" (str(string_of_id id) ++ + str" Not a primitive equality here ") in let sigma = project gls in let env = pf_env gls in match find_positions env sigma t1 t2 with | Inl _ -> errorlabstrm "Inj" - [<'sTR (string_of_id id); - 'sTR" is not a projectable equality but a discriminable one" >] + (str (string_of_id id) ++ + str" is not a projectable equality but a discriminable one") | Inr [] -> errorlabstrm "Equality.inj" - [<'sTR"Nothing to do, it is an equality between convertible terms">] + (str"Nothing to do, it is an equality between convertible terms") | Inr posns -> let e = pf_get_new_id (id_of_string "e") gls in let e_env = push_named_decl (e,None,t) env in @@ -802,7 +802,7 @@ let inj id gls = in if injectors = [] then errorlabstrm "Equality.inj" - [<'sTR "Failed to decompose the equality">]; + (str "Failed to decompose the equality"); tclMAP (fun (injfun,resty) -> let pf = applist(eq.congr (), @@ -816,7 +816,7 @@ let inj id gls = with | UserError("refiner__fail",_) -> errorlabstrm "InjClause" - [< 'sTR (string_of_id id); 'sTR" Not a projectable equality" >] + (str (string_of_id id) ++ str" Not a projectable equality") in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) injectors gls @@ -853,7 +853,7 @@ let decompEqThen ntac id gls = refine (mkApp (pf, [| mkVar id |]))]))) gls | Inr [] -> errorlabstrm "Equality.inj" - [<'sTR"Nothing to do, it is an equality between convertible terms">] + (str"Nothing to do, it is an equality between convertible terms") | Inr posns -> (let e = pf_get_new_id (id_of_string "e") gls in let e_env = push_named_decl (e,None,t) env in @@ -870,7 +870,7 @@ let decompEqThen ntac id gls = in if injectors = [] then errorlabstrm "Equality.decompEqThen" - [<'sTR "Discriminate failed to decompose the equality">]; + (str "Discriminate failed to decompose the equality"); ((tclTHEN (tclMAP (fun (injfun,resty) -> let pf = applist(lbeq.congr (), @@ -901,9 +901,9 @@ let dEqHyp_tac = hide_ident_or_numarg_tactic "DEqHyp" dEqHyp let rewrite_msg = function | None -> - [<'sTR "passed term is not a primitive equality">] + (str "passed term is not a primitive equality") | Some id -> - [<'sTR (string_of_id id); 'sTR "does not satisfy preconditions ">] + (str (string_of_id id) ++ str "does not satisfy preconditions ") let swap_equands gls eqn = let (lbeq,(t,e1,e2)) = @@ -939,12 +939,12 @@ let find_elim sort_of_gl lbeq = (match lbeq.rrec with | Some eq_rec -> (eq_rec (), false) | None -> errorlabstrm "find_elim" - [< 'sTR "this type of elimination is not allowed">]) + (str "this type of elimination is not allowed")) | _ (* Type *) -> (match lbeq.rect with | Some eq_rect -> (eq_rect (), true) | None -> errorlabstrm "find_elim" - [< 'sTR "this type of elimination is not allowed">]) + (str "this type of elimination is not allowed")) (* builds a predicate [e:t][H:(lbeq t e t1)](body e) to be used as an argument for equality dependent elimination principle: @@ -971,7 +971,7 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = find_elim (pf_type_of gls (pf_concl gls)) lbeq with e when catchable_exception e -> errorlabstrm "RevSubstIncConcl" - [< 'sTR "this type of substitution is not allowed">] + (str "this type of substitution is not allowed") in let p = if dep then @@ -1024,7 +1024,7 @@ let find_sigma_data_decompose ex = let subst = match_sigma ex (build_coq_existT_pattern ()) in (build_sigma_type (),subst) with PatternMatchingFailure -> - errorlabstrm "find_sigma_data_decompose" [< >]) + errorlabstrm "find_sigma_data_decompose" (mt ())) let decomp_tuple_term env c t = let rec decomprec inner_code ex exty = @@ -1072,7 +1072,7 @@ let substInConcl eqn gls = let substInHyp eqn id gls = let (lbeq,(t,e1,e2)) = (find_eq_data_decompose eqn) in let body = subst_term e1 (clause_type (Some id) gls) in - if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" [<>]; + if not (dependent (mkRel 1) body) then errorlabstrm "SubstInHyp" (mt ()); (tclTHENS (cut_replacing id (subst1 e2 body)) ([tclIDTAC; (tclTHENS (bareRevSubstInConcl lbeq body (t,e1,e2)) @@ -1088,15 +1088,15 @@ let try_rewrite tac gls = tac gls with | UserError ("find_eq_data_decompose",_) -> errorlabstrm - "try_rewrite" [< 'sTR "Not a primitive equality here">] + "try_rewrite" (str "Not a primitive equality here") | UserError ("swap_equamds",_) -> errorlabstrm - "try_rewrite" [< 'sTR "Not a primitive equality here">] + "try_rewrite" (str "Not a primitive equality here") | UserError("find_eq_elim",s) -> errorlabstrm "try_rew" - [<'sTR "This type of elimination is not allowed ">] + (str "This type of elimination is not allowed ") | e when catchable_exception e -> errorlabstrm "try_rewrite" - [< 'sTR "Cannot find a well type generalisation of the goal that"; - 'sTR " makes progress the proof.">] + (str "Cannot find a well type generalisation of the goal that" ++ + str " makes progress the proof.") (* list_int n 0 [] gives the list [1;2;...;n] *) let rec list_int n cmr l = @@ -1202,7 +1202,7 @@ let general_rewrite_in lft2rgt id (c,lb) gls = (match sub_term_with_unif typ_id mbr_eq with | None -> errorlabstrm "general_rewrite_in" - [<'sTR "Nothing to rewrite in: "; pr_id id>] + (str "Nothing to rewrite in: " ++ pr_id id) | Some (l2,nb_occ) -> (tclTHENSI (tclTHEN @@ -1248,7 +1248,7 @@ let rewrite_in lR com id gls = (try let _ = lookup_named id (pf_env gls) in () with Not_found -> - errorlabstrm "rewrite_in" [< 'sTR"No such hypothesis : " ;pr_id id >]); + errorlabstrm "rewrite_in" (str"No such hypothesis : " ++pr_id id)); let c = pf_interp_constr gls com in let eqn = pf_type_of gls c in try @@ -1259,7 +1259,7 @@ let rewrite_in lR com id gls = ([tclIDTAC ; exact_no_check c])) gls with UserError("SubstInHyp",_) -> tclIDTAC gls) with UserError ("find_eq_data_decompose",_)-> - errorlabstrm "rewrite_in" [< 'sTR"No equality here" >] + errorlabstrm "rewrite_in" (str"No equality here") let subst eqn cls gls = match cls with @@ -1459,7 +1459,7 @@ let sub_list lref i_s i_e = else if (i>=i_s) & (i<i_e) then sub_list_rec (l@[List.nth lref i]) (i+1) else - anomalylabstrm "Equality.sub_list" [<'sTR "Out of range">] + anomalylabstrm "Equality.sub_list" (str "Out of range") in sub_list_rec [] i_s @@ -1514,8 +1514,8 @@ type hint_base = let explicit_hint_base gl = function | By_name id -> begin match rules_of_base id with - | [] -> errorlabstrm "autorewrite" [<'sTR ("Base "^(string_of_id id)^ - " does not exist")>] + | [] -> errorlabstrm "autorewrite" (str ("Base "^(string_of_id id)^ + " does not exist")) | lbs -> lbs end | Explicit lbs -> @@ -1569,7 +1569,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = let cmd = ref cmod and wrn = ref warn in if !cmd=depth_step then begin - wARNING [<'sTR ((string_of_int cglob)^" rewriting(s) carried out") >]; + msg_warning (str ((string_of_int cglob)^" rewriting(s) carried out")); cmd := 0; wrn := true end; @@ -1686,7 +1686,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = in let (gl,lvalid)= let (gl_res,lvalid_res,warn)=iterative_rew 0 0 (0,0,false) [g] [] in - if warn then mSGNL [<>]; + if warn then msgnl (mt ()); (gl_res,lvalid_res) in let validation_fun= @@ -1721,7 +1721,7 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = and int_arg=function | [(Integer n)] -> n | _ -> anomalylabstrm "dyn_autorewrite" - [<'sTR "Bad call of int_arg (not an INTEGER)">] + (str "Bad call of int_arg (not an INTEGER)") and list_args_rest (lstep,evstep) (ostep,evostep) (lrest,evrest) (orest,evorest) (depth,evdepth) = function | [] -> (lstep,ostep,lrest,orest,depth) @@ -1755,13 +1755,13 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = (orest,evorest) (dth,true) tail else errorlabstrm "dyn_autorewrite" - [<'sTR "Depth value lower or equal to 0">]) + (str "Depth value lower or equal to 0")) else anomalylabstrm "dyn_autorewrite" - [<'sTR "Bad call of list_args_rest">] + (str "Bad call of list_args_rest") | _ -> anomalylabstrm "dyn_autorewrite" - [<'sTR "Bad call of list_args_rest">] + (str "Bad call of list_args_rest") and list_args = function | (Redexp (s,lbases))::tail -> if s = "BaseList" then @@ -1774,10 +1774,10 @@ let autorewrite lbases ltacstp opt_step ltacrest opt_rest depth_step gls = ostep (if lrest=[] then None else Some lrest) orest depth) else anomalylabstrm "dyn_autorewrite" - [<'sTR "Bad call of list_args (not a BaseList tagged REDEXP)">] + (str "Bad call of list_args (not a BaseList tagged REDEXP)") | _ -> anomalylabstrm "dyn_autorewrite" - [<'sTR "Bad call of list_args (not a REDEXP)">] + (str "Bad call of list_args (not a REDEXP)") in list_args largs*) |