From 2192f5a2ccedd5e761380f4ef8464236379d4d4a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 21 Jun 2018 17:35:26 +0200 Subject: Inline a function from Quote used in setoid_ring. The code was wrong as it relies once again on term equality and fails on polymorphic constants. Quote is bound to disappear, so we write a correct version of this 10-line function in setoid_ring. --- plugins/setoid_ring/newring.ml | 28 ++++++++++++---------------- 1 file changed, 12 insertions(+), 16 deletions(-) (limited to 'plugins') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 84b29a0bf..eabe2e13f 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -96,25 +96,21 @@ let protect_tac_in map id = (****************************************************************************) +let rec closed_under sigma cset t = + try + let (gr, _) = Termops.global_of_constr sigma t in + Refset_env.mem gr cset + with Not_found -> + match EConstr.kind sigma t with + | Cast(c,_,_) -> closed_under sigma cset c + | App(f,l) -> closed_under sigma cset f && Array.for_all (closed_under sigma cset) l + | _ -> false + let closed_term t l = - let open Quote_plugin in Proofview.tclEVARMAP >>= fun sigma -> - let l = List.map UnivGen.constr_of_global l in - let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) - -(* TACTIC EXTEND echo -| [ "echo" constr(t) ] -> - [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;;*) + let cs = List.fold_right Refset_env.add l Refset_env.empty in + if closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) -(* -let closed_term_ast l = - TacFun([Some(Id.of_string"t")], - TacAtom(Loc.ghost,TacExtend(Loc.ghost,"closed_term", - [Genarg.in_gen Constrarg.wit_constr (mkVar(Id.of_string"t")); - Genarg.in_gen (Genarg.wit_list Constrarg.wit_ref) l]))) -*) let closed_term_ast l = let tacname = { mltac_plugin = "newring_plugin"; -- cgit v1.2.3