Oooops. I forgot the convertibility test that makes the change tactic correct!

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 4a12727c7df207a6b381db4e4b8ae6b680a1c27b..6b5e3f8332c60e21283486461032d020f12ac60d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           let cic =
             if is_uri ast then  (* we have the URI, build the term out of it *)
               try
-                CicUtil.term_of_uri name
+                CicUtil.term_of_uri (UriManager.uri_of_string name)
               with UriManager.IllFormedUri _ ->
                 CicTextualParser2.fail loc "Ill formed URI"
             else
@@ -400,14 +400,18 @@ let interpretate_obj ~context ~env ~uri ~is_path obj =
       (*here the explicit_named_substituion is assumed to be of length 0 *)
       let mutind = Cic.MutInd (uri,0,[]) in
       if params = [] then mutind
-      else Cic.Appl (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
+      else
+       Cic.Appl
+        (mutind::CicUtil.mk_rels (List.length params) (List.length fields)) in
      let con =
       List.fold_left
        (fun t (name,ty) -> Cic.Prod (Cic.Name name,ty,t))
        concl fields' in
      let con' = add_params con in
      let tyl = [name,true,ty',["mk_" ^ name,con']] in
-      Cic.InductiveDefinition (tyl,[],List.length params,[`Class `Record])
+     let field_names = List.map fst fields in
+      Cic.InductiveDefinition
+       (tyl,[],List.length params,[`Class (`Record field_names)])
   | TacticAst.Theorem (_,name,ty,bo) ->
      let ty' = interpretate_term [] env None false ty in
      match bo with
@@ -618,7 +622,7 @@ module Make (C: Callbacks) =
       let uris =
        match uris with
         | [] ->
-           [UriManager.string_of_uri (C.input_or_locate_uri
+           [(C.input_or_locate_uri
             ~title:("URI matching \"" ^ id ^ "\" unknown.") ~id ())]
         | [uri] -> [uri]
         | _ ->
@@ -631,12 +635,12 @@ module Make (C: Callbacks) =
       in
       List.map
         (fun uri ->
-          (uri,
+          (UriManager.string_of_uri uri,
            let term =
              try
                CicUtil.term_of_uri uri
              with exn ->
-               debug_print uri;
+               debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);
                assert false
             in