diff options
| author | Pierre-Marie Pédrot | 2016-11-21 21:33:14 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:30:34 +0100 |
| commit | a327ae04966aa1c7786ae32157516e934068ea89 (patch) | |
| tree | a44bc1804aeb7beb90f4eb45d272c439616af7d3 /plugins/setoid_ring | |
| parent | 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd (diff) | |
Quote API using EConstr.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/g_newring.ml4 | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 3 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.mli | 2 |
3 files changed, 4 insertions, 3 deletions
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 0987c44ae2..89ec4c1c52 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -30,7 +30,7 @@ END TACTIC EXTEND closed_term [ "closed_term" constr(t) "[" ne_reference_list(l) "]" ] -> - [ closed_term t l ] + [ closed_term (EConstr.of_constr t) l ] END open Pptactic diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index b720b2e0a8..2f6c00c9d6 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -97,9 +97,10 @@ let protect_tac_in map id = let closed_term t l = let open Quote_plugin in + Proofview.tclEVARMAP >>= fun sigma -> let l = List.map Universes.constr_of_global l in let cs = List.fold_right Quote.ConstrSet.add l Quote.ConstrSet.empty in - if Quote.closed_under cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) + if Quote.closed_under sigma cs t then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (mt()) (* TACTIC EXTEND echo | [ "echo" constr(t) ] -> diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli index f417c87cde..89538eb24c 100644 --- a/plugins/setoid_ring/newring.mli +++ b/plugins/setoid_ring/newring.mli @@ -19,7 +19,7 @@ val protect_tac_in : string -> Id.t -> unit Proofview.tactic val protect_tac : string -> unit Proofview.tactic -val closed_term : constr -> global_reference list -> unit Proofview.tactic +val closed_term : EConstr.constr -> global_reference list -> unit Proofview.tactic val process_ring_mods : constr_expr ring_mod list -> |