diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/decl_expr.mli | 4 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 8 |
3 files changed, 7 insertions, 7 deletions
diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 5b7f0b4c7..7548c338a 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -83,8 +83,8 @@ type raw_proof_instr = raw_tactic_expr) gen_proof_instr type glob_proof_instr = - ((Id.t*(Genarg.glob_constr_and_expr option)) Loc.located, - Genarg.glob_constr_and_expr, + ((Id.t*(Tacexpr.glob_constr_and_expr option)) Loc.located, + Tacexpr.glob_constr_and_expr, Constrexpr.cases_pattern_expr, Tacexpr.glob_tactic_expr) gen_proof_instr diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 8b90824fd..7ab9488de 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -82,7 +82,7 @@ let pr_intro_as_pat prc _ _ pat = | None -> mt () -ARGUMENT EXTEND with_names TYPED AS intro_pattern_opt PRINTED BY pr_intro_as_pat +ARGUMENT EXTEND with_names TYPED AS simple_intropattern_opt PRINTED BY pr_intro_as_pat | [ "as" simple_intropattern(ipat) ] -> [ Some ipat ] | [] ->[ None ] END diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 03d7c645e..d5c8094d4 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -122,15 +122,15 @@ END;;*) let closed_term_ast l = TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Genarg.wit_constr (mkVar(Id.of_string"t")); - Genarg.in_gen (Genarg.wit_list1 Genarg.wit_ref) l]))) + [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); + Genarg.in_gen (Genarg.wit_list1 Constrarg.wit_ref) l]))) *) let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen (Genarg.glbwit Genarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Genarg.wit_ref)) l]))) + [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); + Genarg.in_gen (Genarg.glbwit (Genarg.wit_list1 Constrarg.wit_ref)) l]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) |