The translation from old aliases to new references is now completely

implemented. It cannot be correct, but it is not supposed to be anyway.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b5c08fba696b979333991ed9f1d661688d9c6fc3..411f393618d54e14b57a833dc5c1b894b5cf351b 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -91,30 +91,42 @@ let ncic_mk_choice = function
       (fun l->assert(l = []);
         let nuri = NUri.uri_of_string uri in
         try
-         let _,height,_,_,_ = NCicEnvironment.get_checked_obj nuri in
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def height))
+         let _,height,_,_,obj = NCicEnvironment.get_checked_obj nuri in
+         let spec =
+          match obj with
+             NCic.Constant (_,_,None,_,_) -> NReference.Decl
+           | NCic.Constant (_,_,Some _,_,_) -> NReference.Def height
+           | NCic.Fixpoint (is_ind,fl,_) ->
+              (* CSC: bug here: name need not be the wanted name
+                 Solution: a real new _reference_ should arrive here *)
+              (match
+                HExtlib.list_index (fun (_,name',_,_,_) -> name=name') fl,is_ind
+               with
+                  None,_ -> assert false
+                | Some (i,(_,_,recno,_,_)),true-> NReference.Fix(i,recno,height)
+                | Some (i,(_,_,_,_,_)),false -> NReference.CoFix i)
+           | NCic.Inductive (inductive,leftno,il,_) ->
+              (match
+                HExtlib.list_index (fun (_,name',_,_) -> name=name') il
+               with
+                  None ->
+                   let cl =
+                    List.concat
+                     (HExtlib.list_mapi (fun (_,_,_,cl) i ->
+                       List.map (fun t -> i,t) cl) il)
+                   in
+                    (match
+                      HExtlib.list_index (fun i,(_,name',_) -> name=name') cl
+                     with
+                        None -> assert false
+                      | Some (j,(i,_)) -> NReference.Con (i,j,leftno))
+                | Some (i,_) -> NReference.Ind (inductive,i,leftno))
+         in
+          NCic.Const (NReference.reference_of_spec nuri spec)
         with
          NCicEnvironment.ObjectNotFound _ ->
-(*
-(*
-        if String.sub uri (String.length uri - 3) 3 = "def" then
-*)
-         let nuri = NUri.uri_of_string uri in(*
-          NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
-         in
-*)
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def 0))
-)
-*)
-(*
-        else
-*)
          let uri = UriManager.uri_of_string uri in
           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
-(*
-*)
 ;;
 
 

diff --git a/helm/software/matita/tests/ng_commands.ma b/helm/software/matita/tests/ng_commands.ma
index dfe92269e4cf081692637219c498d37d1b2e7b13..6a65ea039a68774d0ec0e759b04e1cdf36e7c3a6 100644 (file)
--- a/helm/software/matita/tests/ng_commands.ma
+++ b/helm/software/matita/tests/ng_commands.ma
@@ -38,12 +38,18 @@ alias id "P" = "cic:/matita/tests/ng_commands/P.con".
 
 ndefinition Q: Prop ≝ P.
 
-(*
 nlet rec nzero (n:nat) : nat ≝
  match n with
   [ O ⇒ O
   | S m ⇒ nzero m].
 
+alias id "nzero" = "cic:/matita/tests/ng_commands/nzero.con".
+
+ntheorem nzero_ok: nzero (S (S O)) = O.
+ napply (refl_eq ? O);
+nqed.
+
+(*
 ninductive nnat: Type ≝
    nO: nnat
  | nS: nnat → nnat. *)
\ No newline at end of file