diff options
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/Ring_tac.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/Ring_tac.v b/plugins/setoid_ring/Ring_tac.v index 329fa0ee81..36d1e7c542 100644 --- a/plugins/setoid_ring/Ring_tac.v +++ b/plugins/setoid_ring/Ring_tac.v @@ -460,4 +460,4 @@ Tactic Notation "ring_simplify" "["constr_list(lH)"]" constr_list(rl) "in" hyp(H intro H'; move H' after H; clear H;rename H' into H; - unfold g;clear g.
\ No newline at end of file + unfold g;clear g. diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 0f996c65aa..b8fae2494f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -131,7 +131,7 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in TacFun([Name(Id.of_string"t")], TacML(Loc.tag (tacname, - [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None)); + [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None)); TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)]))) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" @@ -220,7 +220,7 @@ let exec_tactic env evd n f args = let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in let nf c = nf (constr_of c) in - Array.map nf !tactic_res, snd (Evd.universe_context evd) + Array.map nf !tactic_res, snd (Evd.universe_context ~names:[] ~extensible:true evd) let stdlib_modules = [["Coq";"Setoids";"Setoid"]; |