From cc77c0daec24d9b0eeb054b630a9a5b9604c8f4d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 May 2008 18:37:28 +0000
Subject: [PATCH] using the right names in the context to check match
 patterns(better error report) and use the refined matched term to compute the
 type

---
 .../components/cic_unification/cicRefine.ml      | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 45c2d26ea..04d9d7224 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -295,7 +295,6 @@ and type_of_mutual_inductive_constr uri i j ugraph =
  
 and check_branch n context metasenv subst left_args_no actualtype term expectedtype ugraph =
   let module C = Cic in
-    (* let module R = CicMetaSubst in *)
   let module R = CicReduction in
     match R.whd ~subst context expectedtype with
         C.MutInd (_,_,_) ->
@@ -303,7 +302,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
       | C.Appl (C.MutInd (_,_,_)::tl) ->
           let (_,arguments) = split tl left_args_no in
             (n,context,actualtype, arguments@[term]), subst, metasenv, ugraph 
-      | C.Prod (name,so,de) ->
+      | C.Prod (_,so,de) ->
           (* we expect that the actual type of the branch has the due 
              number of Prod *)
           (match R.whd ~subst context actualtype with
@@ -317,7 +316,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
                    (* we should also check that the name variable is anonymous in
                       the actual type de' ?? *)
                    check_branch (n+1) 
-                     ((Some (name,(C.Decl so)))::context) 
+                     ((Some (name',(C.Decl so)))::context) 
                        metasenv subst left_args_no de' term' de ugraph1
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
@@ -583,7 +582,8 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                    context ^ " has type " ^
                   CicMetaSubst.ppterm_in_context ~metasenv subst actual_type
                    context ^ " but is here used with type " ^
-                  CicMetaSubst.ppterm_in_context ~metasenv subst expected_type' context))
+                  CicMetaSubst.ppterm_in_context ~metasenv subst expected_type'
+                  context))
            in
            let rec instantiate_prod t =
             function
@@ -632,7 +632,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                           context)) exn
                   in
                     (p'::pl,j-1,
-                     outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+                     outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
                pl ([],List.length pl,[],subst,metasenv,ugraph3)
            in
            
@@ -817,12 +817,12 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                             context ^ " but is here used with type " ^
                            CicMetaSubst.ppterm_in_context ~metasenv subst instance
                             context)))
-                 (subst,metasenv,ugraph5) pl' outtypeinstances 
+                 (subst,metasenv,ugraph5) pl' outtypeinstances
              in
                C.MutCase (uri, i, outtype, term', pl'),
                  CicReduction.head_beta_reduce
                   (CicMetaSubst.apply_subst subst
-                   (C.Appl(outtype::right_args@[term]))),
+                   (C.Appl(outtype::right_args@[term']))),
                  subst,metasenv,ugraph6)
         | C.Fix (i,fl) ->
             let fl_ty',subst,metasenv,types,ugraph1,len =
@@ -857,7 +857,7 @@ and type_of_aux' ?(clean_dummy_dependent_types=true) ?(localization_tbl = Cic.Ci
                           CicMetaSubst.ppterm_in_context ~metasenv subst ty_of_bo
                            context' ^ " but is here used with type " ^
                           CicMetaSubst.ppterm_in_context ~metasenv subst expected_ty
-                           context))
+                           context'))
                    in 
                      fl @ [bo'] , subst',metasenv',ugraph'
                 ) ([],subst,metasenv,ugraph1) (List.combine fl fl_ty') 
-- 
2.39.2