From 11ca3113365639136cf65a74c345080a9434e69b Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 27 Sep 2013 19:20:27 +0000 Subject: Removing a bunch of generic equalities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16806 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/decl_mode/decl_interp.ml | 8 +++--- plugins/decl_mode/decl_mode.ml | 5 ++-- plugins/decl_mode/decl_proof_instr.ml | 50 +++++++++++++++++------------------ 3 files changed, 31 insertions(+), 32 deletions(-) (limited to 'plugins/decl_mode') diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 52fb935d4..8060dcabf 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -24,7 +24,7 @@ open Misctypes (* INTERN *) -let glob_app (loc,hd,args) = if args =[] then hd else GApp(loc,hd,args) +let glob_app (loc,hd,args) = if List.is_empty args then hd else GApp(loc,hd,args) let intern_justification_items globs = Option.map (List.map (intern_constr globs)) @@ -164,7 +164,7 @@ let decompose_eq env id = let whd = special_whd env typ in match kind_of_term whd with App (f,args)-> - if eq_constr f _eq && (Array.length args)=3 + if eq_constr f _eq && Int.equal (Array.length args) 3 then args.(0) else error "Previous step is not an equality." | _ -> error "Previous step is not an equality." @@ -328,10 +328,10 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let num_params = pinfo.per_nparams in let _ = let expected = mib.Declarations.mind_nparams - num_params in - if List.length params <> expected then + if not (Int.equal (List.length params) expected) then errorlabstrm "suppose it is" (str "Wrong number of extra arguments: " ++ - (if expected = 0 then str "none" else int expected) ++ spc () ++ + (if Int.equal expected 0 then str "none" else int expected) ++ spc () ++ str "expected.") in let app_ind = let rind = GRef (Loc.ghost,Globnames.IndRef pinfo.per_ind) in diff --git a/plugins/decl_mode/decl_mode.ml b/plugins/decl_mode/decl_mode.ml index 0cbd26316..f3c5da2ad 100644 --- a/plugins/decl_mode/decl_mode.ml +++ b/plugins/decl_mode/decl_mode.ml @@ -77,8 +77,9 @@ let get_current_mode () = with Proof_global.NoCurrentProof -> Mode_none let check_not_proof_mode str = - if get_current_mode () = Mode_proof then - error str + match get_current_mode () with + | Mode_proof -> error str + | _ -> () let get_info sigma gl= match Store.get (Goal.V82.extra sigma gl) info with diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index e3ef0671c..cca17a17e 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -77,7 +77,7 @@ let special_nf gl= let is_good_inductive env ind = let mib,oib = Inductive.lookup_mind_specif env ind in - oib.mind_nrealargs = 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) + Int.equal oib.mind_nrealargs 0 && not (Inductiveops.mis_is_recursive (ind,mib,oib)) let check_not_per pts = if not (Proof.is_done pts) then @@ -93,7 +93,7 @@ let mk_evd metalist gls = meta_declare meta typ evd in List.fold_right add_one metalist evd0 -let is_tmp id = (Id.to_string id).[0] = '_' +let is_tmp id = (Id.to_string id).[0] == '_' let tmp_ids gls = let ctx = pf_hyps gls in @@ -289,7 +289,7 @@ type stackd_elt = let rec replace_in_list m l = function [] -> raise Not_found - | c::q -> if m=fst c then l@q else c::replace_in_list m l q + | c::q -> if Int.equal m (fst c) then l@q else c::replace_in_list m l q let enstack_subsubgoals env se stack gls= let hd,params = decompose_app (special_whd gls se.se_type) in @@ -390,7 +390,7 @@ let concl_refiner metas body gls = let nenv = Environ.push_named (_x,None,_A) env in let asort = family_of_sort (Typing.sort_of nenv evd _A) in let nsubst = (n,mkVar _x)::subst in - if rest = [] then + if List.is_empty rest then asort,_A,mkNamedLambda _x _A (subst_meta nsubst body) else let bsort,_B,nbody = @@ -438,7 +438,7 @@ let thus_tac c ctyp submetas gls = find_subsubgoal c ctyp 0 submetas gls with Not_found -> error "I could not relate this statement to the thesis." in - if list = [] then + if List.is_empty list then exact_check proof gls else let refiner = concl_refiner list proof gls in @@ -498,7 +498,7 @@ let decompose_eq id gls = let whd = (special_whd gls typ) in match kind_of_term whd with App (f,args)-> - if eq_constr f _eq && (Array.length args)=3 + if eq_constr f _eq && Int.equal (Array.length args) 3 then (args.(0), args.(1), args.(2)) @@ -672,7 +672,7 @@ let conjunction_arity id gls = Inductive.lookup_mind_specif env ind in let gentypes= Inductive.arities_of_constructors ind (mib,oib) in - let _ = if Array.length gentypes <> 1 then raise Not_found in + let _ = if not (Int.equal (Array.length gentypes) 1) then raise Not_found in let apptype = prod_applist gentypes.(0) params in let rc,_ = Reduction.dest_prod env apptype in List.length rc @@ -791,7 +791,7 @@ let is_rec_pos (main_ind,wft) = None -> false | Some index -> match fst (Rtree.dest_node wft) with - Mrec (_,i) when i = index -> true + Mrec (_,i) when Int.equal i index -> true | _ -> false let rec constr_trees (main_ind,wft) ind = @@ -876,7 +876,7 @@ let per_tac etype casee gls= {pm_stack= Per(etype,per_info,ek,[])::info.pm_stack} gls | Virtual cut -> - assert (cut.cut_stat.st_label=Anonymous); + assert (cut.cut_stat.st_label == Anonymous); let id = pf_get_new_id (Id.of_string "anonymous_matched") gls in let c = mkVar id in let modified_cut = @@ -940,7 +940,7 @@ let rec tree_of_pats ((id,_) as cpl) pats = tree_of_pats cpl (rest_args::stack)) | PatCstr (_,(ind,cnum),args,nam) -> let nexti i ati = - if i = pred cnum then + if Int.equal i (pred cnum) then let nargs = List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Id.Set.singleton id, @@ -985,7 +985,7 @@ let rec add_branch ((id,_) as cpl) pats tree= match tree with Skip_patt (ids,t) -> let nexti i ati = - if i = pred cnum then + if Int.equal i (pred cnum) then let nargs = List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Id.Set.add id ids, @@ -996,11 +996,11 @@ let rec add_branch ((id,_) as cpl) pats tree= skip_args t ids (Array.length ati)) in init_tree ids ind rp nexti | Split_patt (_,ind0,_) -> - if (ind <> ind0) then error + if (not (eq_ind ind ind0)) then error (* this can happen with coercions *) "Case pattern belongs to wrong inductive type."; let mapi i ati bri = - if i = pred cnum then + if Int.equal i (pred cnum) then let nargs = List.map_i (fun j a -> (a,ati.(j))) 0 args in append_branch cpl 0 @@ -1029,14 +1029,14 @@ and append_tree ((id,_) as cpl) depth pats tree = let rec st_assoc id = function [] -> raise Not_found - | st::_ when st.st_label = id -> st.st_it + | st::_ when Name.equal st.st_label id -> st.st_it | _ :: rest -> st_assoc id rest let thesis_for obj typ per_info env= let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in let ind = destInd cind in - let _ = if ind <> per_info.per_ind then + let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in @@ -1170,7 +1170,7 @@ let hrec_for fix_id per_info gls obj_id = let typ=pf_get_hyp_typ gls obj_id in let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in - let ind = destInd cind in assert (ind=per_info.per_ind); + let ind = destInd cind in assert (eq_ind ind per_info.per_ind); let params,args= List.chop per_info.per_nparams all_args in assert begin try List.for_all2 eq_constr params per_info.per_params with @@ -1209,7 +1209,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let env=pf_env gls in let ctyp=pf_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in - let _ = assert (destInd hd = ind) in (* just in case *) + let _ = assert (eq_ind (destInd hd) ind) in (* just in case *) let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_type_of gls c in @@ -1230,7 +1230,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let args_ids = constr_args_ids.(i) in let rec aux n = function [] -> - assert (n=Array.length recargs); + assert (Int.equal n (Array.length recargs)); next_objs,[],nhrec | id :: q -> let objs,recs,nrec = aux (succ n) q in @@ -1302,14 +1302,12 @@ let end_tac et2 gls = | Per(et',pi,ek,clauses)::_ -> (et',pi,ek,clauses) | [] -> anomaly (Pp.str "This case should already be trapped") in - let et = - if et1 <> et2 then - match et1 with - ET_Case_analysis -> - error "\"end cases\" expected." - | ET_Induction -> - error "\"end induction\" expected." - else et1 in + let et = match et1, et2 with + | ET_Case_analysis, ET_Case_analysis -> et1 + | ET_Induction, ET_Induction -> et1 + | ET_Case_analysis, _ -> error "\"end cases\" expected." + | ET_Induction, _ -> error "\"end induction\" expected." + in tclTHEN tcl_erase_info begin -- cgit v1.2.3