diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/Inv.v | 10 | ||||
| -rw-r--r-- | tactics/dhyp.ml | 4 | ||||
| -rw-r--r-- | tactics/inv.ml | 8 | ||||
| -rw-r--r-- | tactics/inv.mli | 2 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 18 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 16 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tauto.ml4 | 4 |
8 files changed, 32 insertions, 32 deletions
diff --git a/tactics/Inv.v b/tactics/Inv.v index 39a434b010..2b9271aca5 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -49,7 +49,7 @@ Grammar tactic simple_tactic: ast := | inv_using [ inversion_com($ic) identarg($id) "using" constrarg($c) ] -> case [$ic] of - Inversion -> [(UseInversionLemma $id $c)] + "Inversion" -> [(UseInversionLemma $id $c)] esac | inv_num_using [ inversion_com($ic) pure_numarg($n) "using" constrarg($c) ] @@ -61,13 +61,13 @@ Grammar tactic simple_tactic: ast := [ inversion_com($ic) identarg($id) "using" constrarg($c) "in" ne_identarg_list($l) ] -> case [$ic] of - Inversion -> [(UseInversionLemmaIn $id $c ($LIST $l))] + "Inversion" -> [(UseInversionLemmaIn $id $c ($LIST $l))] esac with inversion_com: ast := - simple_inv [ "Simple" "Inversion" ] -> [ HalfInversion ] -| inversion_com [ "Inversion" ] -> [ Inversion ] -| inv_clear [ "Inversion_clear" ] -> [ InversionClear ]. + simple_inv [ "Simple" "Inversion" ] -> [ "HalfInversion" ] +| inversion_com [ "Inversion" ] -> [ "Inversion" ] +| inv_clear [ "Inversion_clear" ] -> [ "InversionClear" ]. Grammar vernac vernac: ast := diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 211ecbf6dd..839c639789 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -253,8 +253,8 @@ let match_dpat dp cls gls = let applyDestructor cls discard dd gls = let mvb = match_dpat dd.d_pat cls gls in let astb = match cls with - | Some id -> ["$0", Vast (nvar (string_of_id id))] - | None -> ["$0", Vast (nvar "$0")] in + | Some id -> ["$0", Vast (nvar id)] + | None -> ["$0", Vast (nvar (id_of_string "$0"))] in (* TODO: find the real location *) let tcom = match Ast.eval_act dummy_loc astb dd.d_code with | Vast tcom -> tcom diff --git a/tactics/inv.ml b/tactics/inv.ml index 4e0c39ab26..3fbe8e8eef 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -413,9 +413,9 @@ let inv gene com status id = in fun gls -> try tac gls with e -> wrap_inv_error id e -let hinv_kind = Identifier (id_of_string "HalfInversion") -let inv_kind = Identifier (id_of_string "Inversion") -let invclr_kind = Identifier (id_of_string "InversionClear") +let hinv_kind = Quoted_string "HalfInversion" +let inv_kind = Quoted_string "Inversion" +let invclr_kind = Quoted_string "InversionClear" let com_of_id id = if id = hinv_kind then None @@ -519,6 +519,6 @@ let invIn_tac = in fun com id hl -> gentac - ((Identifier (id_of_string com)) + ((Identifier com) ::(Identifier id) ::(List.map (fun id -> (Identifier id)) hl)) diff --git a/tactics/inv.mli b/tactics/inv.mli index ed0dc1de0c..792f132613 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -24,4 +24,4 @@ val half_dinv_with : identifier -> constr -> tactic val dinv_with : identifier -> constr -> tactic val dinv_clear_with : identifier -> constr -> tactic -val invIn_tac : string -> identifier -> identifier list -> tactic +val invIn_tac : identifier -> identifier -> identifier list -> tactic diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index dd35bc58f4..613c0a475c 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -39,7 +39,7 @@ type morphism = let constr_of c = Astterm.interp_constr Evd.empty (Global.env()) c let constant dir s = - let dir = "Coq"::"Setoid"::dir in + let dir = make_dirpath (List.map id_of_string ("Coq"::"Setoid"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id @@ -47,7 +47,7 @@ let constant dir s = anomaly ("Setoid: cannot find "^(Nametab.string_of_qualid (Nametab.make_qualid dir id))) let global_constant dir s = - let dir = "Coq"::"Init"::dir in + let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::dir)) in let id = id_of_string s in try Declare.global_reference_in_absolute_module dir id @@ -206,7 +206,7 @@ let gen_eq_lem_name = let i = ref 0 in function () -> incr i; - id_of_string ("setoid_eq_ext"^(string_of_int !i)) + make_ident "setoid_eq_ext" (Some !i) let add_setoid a aeq th = if setoid_table_mem a @@ -289,11 +289,11 @@ let check_is_dependent t n = in aux t 0 n let gen_lem_name m = match kind_of_term m with - | IsVar id -> id_of_string ((string_of_id id)^"_ext") - | IsConst (sp, _) -> id_of_string ((string_of_id(basename sp))^"_ext") - | IsMutInd ((sp, i), _) -> id_of_string ((string_of_id(basename sp))^(string_of_int i)^"_ext") - | IsMutConstruct (((sp,i),j), _) -> id_of_string - ((string_of_id(basename sp))^(string_of_int i)^(string_of_int i)^"_ext") + | IsVar id -> add_suffix id "_ext" + | IsConst (sp, _) -> add_suffix (basename sp) "_ext" + | IsMutInd ((sp, i), _) -> add_suffix (basename sp) ((string_of_int i)^"_ext") + | IsMutConstruct (((sp,i),j), _) -> add_suffix + (basename sp) ((string_of_int i)^(string_of_int i)^"_ext") | _ -> errorlabstrm "New Morphism" [< 'sTR "The term "; prterm m; 'sTR "is not a known name">] let gen_lemma_tail m lisset body n = @@ -449,7 +449,7 @@ let add_morphism lem_name (m,profil) = (if (eq_constr body mkProp) then (let lem_2 = gen_lem_iff env m mext args_t poss in - let lem2_name = (id_of_string ((string_of_id lem_name)^"2")) in + let lem2_name = add_suffix lem_name "2" in let _ = Declare.declare_constant lem2_name ((Declare.ConstantEntry {Declarations.const_entry_body = lem_2; Declarations.const_entry_type = None}), diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cb86443838..9d8f07d78f 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -312,12 +312,6 @@ let last_arg c = match kind_of_term c with let general_elim_then_using elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl = let ((ity,_,_),t) = reduce_to_ind_goal gl (pf_type_of gl c) in - let name_elim = - (match kind_of_term elim with - | IsConst (sp,_) -> id_of_string (string_of_path sp) - | IsVar id -> id - | _ -> id_of_string " ") - in (* applying elimination_scheme just a little modified *) let (wc,kONT) = startWalk gl in let indclause = mk_clenv_from wc (c,t) in @@ -332,8 +326,14 @@ let general_elim_then_using let p, _ = decomp_app (clenv_template_type elimclause).rebus in match kind_of_term p with | IsMeta p -> p - | _ -> error ("The elimination combinator " ^ - (string_of_id name_elim) ^ " is not known") + | _ -> + let name_elim = + match kind_of_term elim with + | IsConst (sp,_) -> string_of_path sp + | IsVar id -> string_of_id id + | _ -> "\b" + in + error ("The elimination combinator " ^ name_elim ^ " is not known") in let elimclause' = clenv_fchain indmv elimclause indclause' in let elimclause' = clenv_constrain_with_bindings elimbindings elimclause' in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bffbfea4ce..12b41b6027 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1823,7 +1823,7 @@ let abstract_subproof name tac gls = in if occur_existential concl then error "Abstract cannot handle existentials"; let lemme = - start_proof na Declare.NeverDischarge current_sign concl; + start_proof na NeverDischarge current_sign concl; let _,(const,strength) = try by (tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac)); diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 7edf1610e5..5996449275 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -115,7 +115,7 @@ let rec intuition_main () = let unfold_not_iff = function | None -> interp <:tactic<Unfold not iff>> | Some id -> - let ast_id = nvar (string_of_id id) in + let ast_id = nvar id in interp <:tactic<Unfold not iff in $ast_id>> let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido) @@ -123,7 +123,7 @@ let reduction_not_iff = Tacticals.onAllClauses (fun ido -> unfold_not_iff ido) let compute = function | None -> interp <:tactic<Compute>> | Some id -> - let ast_id = nvar (string_of_id id) in + let ast_id = nvar id in interp <:tactic<Compute in $ast_id>> let reduction = Tacticals.onAllClauses (fun ido -> compute ido) |