diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 7 | ||||
| -rw-r--r-- | plugins/xml/acic2Xml.ml4 | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 355a180052..f16c298af9 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -35,10 +35,13 @@ open Misctypes (****************************************************************************) (* controlled reduction *) -let mark_arg i c = mkEvar(i,[|c|]) +(** ppedrot: something dubious here, we're obviously using evars the wrong + way. FIXME! *) + +let mark_arg i c = mkEvar(Evar.unsafe_of_int i,[|c|]) let unmark_arg f c = match destEvar c with - | (i,[|c|]) -> f i c + | (i,[|c|]) -> f (Evar.repr i) c | _ -> assert false type protect_flag = Eval|Prot|Rec diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index 9d3a10dbae..73f113d6ab 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -26,7 +26,7 @@ let rec find_last_id = | _::tl -> find_last_id tl ;; -let export_existential = string_of_int +let export_existential ev = string_of_int (Evar.repr ev) let print_term ids_to_inner_sorts = let rec aux = |