nasty change in the lexer/parser:

[helm.git] / helm / software / components / ng_refiner / nCicRefiner.ml

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index a724ae1cb6770c09559fa5a26bdfae55637d441c..64911e198337ef472e010f2324dec30180fa7ab8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -424,6 +424,20 @@ and sort_of_prod
          (NCicPp.ppterm ~subst ~metasenv ~context y) 
          (NCicPp.ppterm ~subst ~metasenv ~context x))))
 
+and guess_name subst ctx ty = 
+  let aux initial = "#" ^ String.make 1 initial in
+  match ty with
+  | C.Const (NReference.Ref (u,_))
+  | C.Appl (C.Const (NReference.Ref (u,_)) :: _) ->
+      aux (String.sub (NUri.name_of_uri u) 0 1).[0] 
+  | C.Prod _ -> aux 'f' 
+  | C.Meta (n,lc) -> 
+      (try
+         let _,_,t,_ = NCicUtils.lookup_subst n subst in
+         guess_name subst ctx (NCicSubstitution.subst_meta lc t)
+      with NCicUtils.Subst_not_found _ -> aux 'M')
+  | _ -> aux 'H' 
+
 and eat_prods hdb
   ~localise ~look_for_coercion metasenv subst context orig_he he ty_he args 
 =
@@ -443,11 +457,12 @@ and eat_prods hdb
           let metasenv, subst, arg, ty_arg = 
             typeof hdb ~look_for_coercion ~localise 
               metasenv subst context arg None in
+          let name = guess_name subst context ty_arg in
           let metasenv, _, meta, _ = 
             NCicMetaSubst.mk_meta metasenv 
-              (("_",C.Decl ty_arg) :: context) `Type
+              ((name,C.Decl ty_arg) :: context) `Type
           in
-          let flex_prod = C.Prod ("_", ty_arg, meta) in
+          let flex_prod = C.Prod (name, ty_arg, meta) in
           (* next line grants that ty_args is a type *)
           let metasenv,subst, flex_prod, _ =
            typeof hdb ~look_for_coercion ~localise metasenv subst