In the case type_of constructor with expected type T, T is now put in whd to

find an expected inductive type.

diff --git a/matita/components/ng_refiner/nCicRefiner.ml b/matita/components/ng_refiner/nCicRefiner.ml
index 76a04c9e6abe56d965cc3be8361a8db60b16d5c6..56632b03ff658e8c92419ff3f009cbe41ebaa114 100644 (file)
--- a/matita/components/ng_refiner/nCicRefiner.ml
+++ b/matita/components/ng_refiner/nCicRefiner.ml
@@ -319,32 +319,36 @@ let rec typeof rdb
          with Uncertain _ | RefineFailure _ -> refine_appl metasenv subst args
        else
         (* CSC: whd can be useful on he and expty ... *)
-        (match he, expty with
-            C.Const (Ref.Ref (uri1,Ref.Con _)),
-             Some (C.Appl (C.Const (Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
-             when NUri.eq uri1 uri2 ->
-              (try
-               let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys ref in
-               let leftargs,rightargs = HExtlib.split_nth leftno args in
-               let leftexpargs,_ = HExtlib.split_nth leftno expargs in
-               let metasenv,subst,leftargs_rev =
-                List.fold_left2
-                 (fun (metasenv,subst,args) arg exparg ->
-                   let metasenv,subst,arg,_ =
-                    typeof_aux metasenv subst context None arg in
-                   let metasenv,subst =
-                    NCicUnification.unify rdb metasenv subst context arg exparg
-                   in
-                    metasenv,subst,arg::args
-                 ) (metasenv,subst,[]) leftargs leftexpargs
-               in
-                (* some checks are re-done here, but it would be complex to
-                 * avoid them (e.g. we did not check yet that the constructor
-                 * is a construtor for that inductive type) *)
-                refine_appl metasenv subst ((List.rev leftargs_rev)@rightargs)
-              with
-               | Sys.Break as exn -> raise exn
-               | _ -> refine_appl metasenv subst args (* to try coercions *))
+        (match he with
+            C.Const (Ref.Ref (uri1,Ref.Con _)) -> (
+             match
+              HExtlib.map_option (NCicReduction.whd ~subst context) expty
+             with
+                Some (C.Appl(C.Const(Ref.Ref (uri2,Ref.Ind _) as ref)::expargs))
+                when NUri.eq uri1 uri2 ->
+                (try
+                 let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys ref in
+                 let leftargs,rightargs = HExtlib.split_nth leftno args in
+                 let leftexpargs,_ = HExtlib.split_nth leftno expargs in
+                 let metasenv,subst,leftargs_rev =
+                  List.fold_left2
+                   (fun (metasenv,subst,args) arg exparg ->
+                     let metasenv,subst,arg,_ =
+                      typeof_aux metasenv subst context None arg in
+                     let metasenv,subst =
+                      NCicUnification.unify rdb metasenv subst context arg exparg
+                     in
+                      metasenv,subst,arg::args
+                   ) (metasenv,subst,[]) leftargs leftexpargs
+                 in
+                  (* some checks are re-done here, but it would be complex to
+                   * avoid them (e.g. we did not check yet that the constructor
+                   * is a construtor for that inductive type) *)
+                  refine_appl metasenv subst ((List.rev leftargs_rev)@rightargs)
+                with
+                 | Sys.Break as exn -> raise exn
+                 | _ -> refine_appl metasenv subst args (* to try coercions *))
+              | _ -> refine_appl metasenv subst args)
           | _ -> refine_appl metasenv subst args)
    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
    | C.Match (Ref.Ref (_,Ref.Ind (_,tyno,_)) as r,