From cf5d6fab96c47ccb7d623d72742717d9b08bae7b Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 20 Jul 2004 12:50:13 +0000
Subject: [PATCH] Subst has been added to the kernel.

---
 helm/ocaml/cic_proof_checking/cicPp.ml        |  18 +
 helm/ocaml/cic_proof_checking/cicPp.mli       |  30 +-
 .../ocaml/cic_proof_checking/cicReduction.mli |   5 +-
 .../cic_proof_checking/cicReductionMachine.ml |  36 +-
 .../cic_proof_checking/cicTypeChecker.ml      | 473 +++++++++---------
 .../cic_proof_checking/cicTypeChecker.mli     |   2 +-
 helm/ocaml/cic_unification/cicMetaSubst.ml    | 156 +++++-
 helm/ocaml/cic_unification/cicMetaSubst.mli   |  10 +-
 helm/ocaml/cic_unification/cicMkImplicit.ml   |  12 +-
 helm/ocaml/cic_unification/cicRefine.ml       | 112 +++--
 helm/ocaml/cic_unification/cicUnification.ml  | 413 ++++++++-------
 11 files changed, 772 insertions(+), 495 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index 8172b47f7..b9a5b72f4 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -193,6 +193,24 @@ let ppinductiveType (typename, inductive, arity, cons) =
    cons ""
 ;;
 
+let ppcontext ?(sep = "\n") context =
+ let separate s = if s = "" then "" else s ^ sep in
+ fst (List.fold_right 
+   (fun context_entry (i,name_context) ->
+     match context_entry with
+        Some (n,Cic.Decl t) ->
+         Printf.sprintf "%s%s : %s" (separate i) (ppname n)
+          (pp t name_context), (Some n)::name_context
+      | Some (n,Cic.Def (bo,ty)) ->
+         Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
+          (match ty with
+              None -> "_"
+            | Some ty -> pp ty name_context)
+          (pp bo name_context), (Some n)::name_context
+       | None ->
+          Printf.sprintf "%s_ :? _" (separate i), None::name_context
+    ) context ("",[]))
+
 (* ppobj obj  returns a string with describing the cic object obj in a syntax *)
 (* similar to the one used by Coq                                             *)
 let ppobj obj =
diff --git a/helm/ocaml/cic_proof_checking/cicPp.mli b/helm/ocaml/cic_proof_checking/cicPp.mli
index 371b75e29..417378d29 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.mli
+++ b/helm/ocaml/cic_proof_checking/cicPp.mli
@@ -23,25 +23,27 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This module implements a very simple Coq-like pretty printer that, given   *)
-(* an object of cic (internal representation) returns a string describing the *)
-(* object in a syntax similar to that of coq                                  *)
-(*                                                                            *)
-(******************************************************************************)
+(*****************************************************************************)
+(*                                                                           *)
+(*                               PROJECT HELM                                *)
+(*                                                                           *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>              *)
+(*                                 24/01/2000                                *)
+(*                                                                           *)
+(* This module implements a very simple Coq-like pretty printer that, given  *)
+(* an object of cic (internal representation) returns a string describing the*)
+(* object in a syntax similar to that of coq                                 *)
+(*                                                                           *)
+(*****************************************************************************)
 
-(* ppobj obj  returns a string with describing the cic object obj in a syntax *)
-(* similar to the one used by Coq                                             *)
+(* ppobj obj  returns a string with describing the cic object obj in a syntax*)
+(* similar to the one used by Coq                                            *)
 val ppobj : Cic.obj -> string
 
 val ppterm : Cic.term -> string
 
+val ppcontext : ?sep:string -> Cic.context -> string 
+
 (* Required only by the topLevel. It is the generalization of ppterm to *)
 (* work with environments.                                              *)
 val pp : Cic.term -> (Cic.name option) list -> string
diff --git a/helm/ocaml/cic_proof_checking/cicReduction.mli b/helm/ocaml/cic_proof_checking/cicReduction.mli
index 7a6255003..eaa2265ba 100644
--- a/helm/ocaml/cic_proof_checking/cicReduction.mli
+++ b/helm/ocaml/cic_proof_checking/cicReduction.mli
@@ -29,5 +29,6 @@ exception ReferenceToVariable
 exception ReferenceToCurrentProof
 exception ReferenceToInductiveDefinition
 val fdebug : int ref
-val whd : Cic.context -> Cic.term -> Cic.term
-val are_convertible : Cic.context -> Cic.term -> Cic.term -> bool
+val whd : ?subst:Cic.substitution -> Cic.context -> Cic.term -> Cic.term
+val are_convertible : 
+  ?subst:Cic.substitution -> ?metasenv:Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> bool
diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e963ddce9..4b8099fed 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -498,7 +498,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
    unwind' 0 
   ;;
   
-  let reduce context : config -> Cic.term = 
+  let reduce ?(subst = []) context : config -> Cic.term = 
    let module C = Cic in
    let module S = CicSubstitution in 
    let rec reduce =
@@ -542,9 +542,13 @@ if List.mem uri params then prerr_endline "---- OK2" ;
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
-     | (k, e, ens, (C.Meta _ as t), s) ->
-        let t' = unwind k e ens t in
-         if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
+     | (k, e, ens, (C.Meta (n,l) as t), s) ->
+        (try 
+	   let (_, term) = CicUtil.lookup_subst n subst in
+           reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
+	 with  CicUtil.Subst_not_found _ ->
+           let t' = unwind k e ens t in
+           if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
      | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
      | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
      | (k, e, ens, (C.Cast (te,ty) as t), s) ->
@@ -722,10 +726,10 @@ if List.mem uri params then prerr_endline "---- OK2" ;
      | (uri,t)::tl ->
          push_exp_named_subst k e ((uri,RS.to_ens (unwind k e ens t))::ens) tl
    in
-    reduce
+    reduce 
   ;;
   
-  let rec whd context t = reduce context (0, [], [], t, []);;
+  let rec whd ?(subst=[]) context t = reduce ~subst context (0, [], [], t, []);;
   
 (* DEBUGGING ONLY
 let whd context t =
@@ -769,7 +773,7 @@ module R = Reduction(ClosuresOnStackByValueFromEnvOrEnsStrategy);;
 let whd = R.whd;;
 
 (* t1, t2 must be well-typed *)
-let are_convertible =
+let are_convertible ?(subst=[]) ?(metasenv=[]) =
  let module U = UriManager in
  let rec aux test_equality_only context t1 t2 =
   let aux2 test_equality_only t1 t2 =
@@ -792,8 +796,10 @@ let are_convertible =
               with
                Invalid_argument _ -> false
              )
-        | (C.Meta (n1,l1), C.Meta (n2,l2)) -> 
+        | (C.Meta (n1,l1), C.Meta (n2,l2)) ->
             n1 = n2 &&
+             let l1 = CicUtil.clean_up_local_context subst metasenv n1 l1 in
+             let l2 = CicUtil.clean_up_local_context subst metasenv n2 l2 in
              List.fold_left2
               (fun b t1 t2 ->
                 b &&
@@ -900,10 +906,18 @@ let are_convertible =
   in
    if aux2 test_equality_only t1 t2 then true
    else
-    begin
+     begin
      debug t1 [t2] "PREWHD";
-     let t1' = whd context t1 in
-     let t2' = whd context t2 in
+     (* 
+     (match t1 with 
+	 Cic.Meta _ -> 
+	   prerr_endline (CicPp.ppterm t1);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t1));
+	   prerr_endline (CicPp.ppterm t2);
+	   prerr_endline (CicPp.ppterm (whd ~subst context t2))
+       | _ -> ()); *)
+     let t1' = whd ~subst context t1 in
+     let t2' = whd ~subst context t2 in
       debug t1' [t2'] "POSTWHD";
       aux2 test_equality_only t1' t2'
     end
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 1577b2f3f..5715778fb 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -592,11 +592,11 @@ and recursive_args context n nn te =
    | C.Fix _
    | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
 
-and get_new_safes context p c rl safes n nn x =
+and get_new_safes ?(subst = []) context p c rl safes n nn x =
  let module C = Cic in
  let module U = UriManager in
  let module R = CicReduction in
-  match (R.whd context c, R.whd context p, rl) with
+  match (R.whd ~subst context c, R.whd ~subst context p, rl) with
      (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
        (* we are sure that the two sources are convertible because we *)
        (* have just checked this. So let's go along ...               *)
@@ -606,7 +606,7 @@ and get_new_safes context p c rl safes n nn x =
         let safes'' =
          if b then 1::safes' else safes'
         in
-         get_new_safes ((Some (name,(C.Decl so)))::context)
+         get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
           ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
    | (C.Prod _, (C.MutConstruct _ as e), _)
    | (C.Prod _, (C.Rel _ as e), _)
@@ -623,30 +623,30 @@ and get_new_safes context p c rl safes n nn x =
          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
            (CicPp.ppterm c) (CicPp.ppterm p)))
 
-and split_prods context n te =
+and split_prods ?(subst = []) context n te =
  let module C = Cic in
  let module R = CicReduction in
   match (n, R.whd context te) with
      (0, _) -> context,te
    | (n, C.Prod (name,so,ta)) when n > 0 ->
-       split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
+       split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
    | (_, _) -> raise (AssertFailure "8")
 
-and eat_lambdas context n te =
+and eat_lambdas ?(subst = []) context n te =
  let module C = Cic in
  let module R = CicReduction in
-  match (n, R.whd context te) with
+  match (n, R.whd ~subst context te) with
      (0, _) -> (te, 0, context)
    | (n, C.Lambda (name,so,ta)) when n > 0 ->
       let (te, k, context') =
-       eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
+       eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
       in
        (te, k + 1, context')
    | (n, te) ->
        raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 
-(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
-and check_is_really_smaller_arg context n nn kl x safes te =
+(*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) 
+and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
  (*CSC: cfr guarded_by_destructors                             *)
  let module C = Cic in
@@ -660,25 +660,25 @@ and check_is_really_smaller_arg context n nn kl x safes te =
    | C.Implicit _
    | C.Cast _
 (*   | C.Cast (te,ty) ->
-      check_is_really_smaller_arg n nn kl x safes te &&
-       check_is_really_smaller_arg n nn kl x safes ty*)
+      check_is_really_smaller_arg ~subst n nn kl x safes te &&
+       check_is_really_smaller_arg ~subst n nn kl x safes ty*)
 (*   | C.Prod (_,so,ta) ->
-      check_is_really_smaller_arg n nn kl x safes so &&
-       check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
+      check_is_really_smaller_arg ~subst n nn kl x safes so &&
+       check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
         (List.map (fun x -> x + 1) safes) ta*)
    | C.Prod _ -> raise (AssertFailure "10")
    | C.Lambda (name,so,ta) ->
-      check_is_really_smaller_arg context n nn kl x safes so &&
-       check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
+      check_is_really_smaller_arg ~subst context n nn kl x safes so &&
+       check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ta) ->
-      check_is_really_smaller_arg context n nn kl x safes so &&
-       check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
+      check_is_really_smaller_arg ~subst context n nn kl x safes so &&
+       check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl (he::_) ->
       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
       (*CSC: solo perche' non abbiamo trovato controesempi            *)
-      check_is_really_smaller_arg context n nn kl x safes he
+      check_is_really_smaller_arg ~subst context n nn kl x safes he
    | C.Appl [] -> raise (AssertFailure "11")
    | C.Const _
    | C.MutInd _ -> raise (AssertFailure "12")
@@ -697,7 +697,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -708,7 +708,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
             if not isinductive then
               List.fold_right
                (fun p i ->
-                 i && check_is_really_smaller_arg context n nn kl x safes p)
+                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
                pl true
             else
               List.fold_right
@@ -718,10 +718,10 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                    recursive_args tys 0 len debrujinedte
                  in
                   let (e,safes',n',nn',x',context') =
-                   get_new_safes context p c rl' safes n nn x
+                   get_new_safes ~subst context p c rl' safes n nn x
                   in
                    i &&
-                   check_is_really_smaller_arg context' n' nn' kl x' safes' e
+                   check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
            let (tys,len,isinductive,paramsno,cl) =
@@ -735,7 +735,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -746,7 +746,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
             if not isinductive then
               List.fold_right
                (fun p i ->
-                 i && check_is_really_smaller_arg context n nn kl x safes p)
+                 i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
                pl true
             else
               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
@@ -761,12 +761,12 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                    get_new_safes context p c rl' safes n nn x
                   in
                    i &&
-                   check_is_really_smaller_arg context' n' nn' kl x' safes' e
+                   check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
                ) (List.combine pl cl) true
         | _ ->
           List.fold_right
            (fun p i ->
-             i && check_is_really_smaller_arg context n nn kl x safes p
+             i && check_is_really_smaller_arg ~subst context n nn kl x safes p
            ) pl true
       )
    | C.Fix (_, fl) ->
@@ -779,7 +779,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i &&
-            check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
+            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
    | C.CoFix (_, fl) ->
@@ -792,11 +792,11 @@ and check_is_really_smaller_arg context n nn kl x safes te =
         List.fold_right
          (fun (_,ty,bo) i ->
            i &&
-            check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
+            check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
              x_plus_len safes' bo
          ) fl true
 
-and guarded_by_destructors context n nn kl x safes =
+and guarded_by_destructors ?(subst = []) context n nn kl x safes =
  let module C = Cic in
  let module U = UriManager in
   function
@@ -835,7 +835,7 @@ and guarded_by_destructors context n nn kl x safes =
          (fun param i ->
            i && guarded_by_destructors context n nn kl x safes param
          ) tl true &&
-         check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
+         check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
    | C.Appl tl ->
       List.fold_right
        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
@@ -863,8 +863,8 @@ and guarded_by_destructors context n nn kl x safes =
                     List.map
                      (fun (id,ty) ->
                       let debrujinedty = debrujin_constructor uri len ty in
-                       (id, snd (split_prods tys paramsno ty),
-                        snd (split_prods tys paramsno debrujinedty)
+                       (id, snd (split_prods ~subst tys paramsno ty),
+                        snd (split_prods ~subst tys paramsno debrujinedty)
                        )) cl
                    in
                     (tys,len,isinductive,paramsno,cl')
@@ -905,7 +905,7 @@ and guarded_by_destructors context n nn kl x safes =
                   let cl' =
                    List.map
                     (fun (id,ty) ->
-                      (id, snd (split_prods tys paramsno ty))) cl
+                      (id, snd (split_prods ~subst tys paramsno ty))) cl
                   in
                    (tys,List.length tl,isinductive,paramsno,cl')
              | _ ->
@@ -1299,11 +1299,11 @@ and type_of_branch context argsno need_dummy outtype term constype =
 metavariable is consitent - up to relocation via the relocation list l -
 with the actual context *)
 
-and check_metasenv_consistency metasenv context canonical_context l =
+and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l =
   let module C = Cic in
   let module R = CicReduction in
   let module S = CicSubstitution in
-   let lifted_canonical_context = 
+    let lifted_canonical_context = 
     let rec aux i =
      function
         [] -> []
@@ -1315,30 +1315,41 @@ and check_metasenv_consistency metasenv context canonical_context l =
       | (Some (n,C.Def (t,Some ty)))::tl ->
          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
     in
-     aux 1 canonical_context
+     aux 1 canonical_context 
    in
     List.iter2 
      (fun t ct -> 
         match (t,ct) with
          | _,None -> ()
          | Some t,Some (_,C.Def (ct,_)) ->
-            if not (R.are_convertible context t ct) then
+            if not (R.are_convertible ~subst ~metasenv context t ct) then
               raise (TypeCheckerFailure (sprintf
                 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
                 (CicPp.ppterm ct) (CicPp.ppterm t)))
          | Some t,Some (_,C.Decl ct) ->
-             let type_t = type_of_aux' metasenv context t in
-             if not (R.are_convertible context type_t ct) then
+             let type_t = type_of_aux' ~subst metasenv context t in
+             if not (R.are_convertible ~subst ~metasenv context type_t ct) then
+	       (* debug *)
+	       (
+                 (*
+		 (match type_t with 
+		     Cic.Meta (n,l) ->
+		       try 
+			 let (cc, ecco) = CicUtil.lookup_subst n subst in
+			 prerr_endline (CicPp.ppterm ecco)
+		       with CicUtil.Subst_not_found _ ->
+                         prerr_endline "Non lo trovo"
+		    | _ -> ()); *)
               raise (TypeCheckerFailure (sprintf
                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
-                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
+                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))))
          | None, _  ->
              raise (TypeCheckerFailure
               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
      ) l lifted_canonical_context 
 
 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
-and type_of_aux' metasenv context t =
+and type_of_aux' ?(subst = []) metasenv context t =
  let rec type_of_aux context =
   let module C = Cic in
   let module R = CicReduction in
@@ -1360,16 +1371,23 @@ and type_of_aux' metasenv context t =
        )
     | C.Var (uri,exp_named_subst) ->
       incr fdebug ;
-      check_exp_named_subst context exp_named_subst ;
+      check_exp_named_subst ~subst context exp_named_subst ;
       let ty =
        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
       in
        decr fdebug ;
        ty
     | C.Meta (n,l) -> 
-       let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
-        check_metasenv_consistency metasenv context canonical_context l;
-        CicSubstitution.lift_meta l ty
+       (try
+          let (canonical_context, term) = CicUtil.lookup_subst n subst in
+          check_metasenv_consistency 
+	    ~subst metasenv context canonical_context l;
+          type_of_aux context (CicSubstitution.lift_meta l term)
+	with CicUtil.Subst_not_found _ ->
+	  let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
+            check_metasenv_consistency 
+	      ~subst metasenv context canonical_context l;
+            CicSubstitution.lift_meta l ty)
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in
@@ -1382,7 +1400,7 @@ and type_of_aux' metasenv context t =
     | C.Implicit _ -> raise (AssertFailure "21")
     | C.Cast (te,ty) as t ->
        let _ = type_of_aux context ty in
-        if R.are_convertible context (type_of_aux context te) ty then
+        if R.are_convertible ~subst ~metasenv context (type_of_aux context te) ty then
           ty
         else
           raise (TypeCheckerFailure
@@ -1390,11 +1408,11 @@ and type_of_aux' metasenv context t =
     | C.Prod (name,s,t) ->
        let sort1 = type_of_aux context s
        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
-       let res = sort_of_prod context (name,s) (sort1,sort2) in
+       let res = sort_of_prod ~subst context (name,s) (sort1,sort2) in
       res
    | C.Lambda (n,s,t) ->
        let sort1 = type_of_aux context s in
-       (match R.whd context sort1 with
+       (match R.whd ~subst context sort1 with
            C.Meta _
          | C.Sort _ -> ()
          | _ ->
@@ -1426,11 +1444,11 @@ and type_of_aux' metasenv context t =
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux context he in
       let tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
-       eat_prods context hetype tlbody_and_type
+       eat_prods ~subst context hetype tlbody_and_type
    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
    | C.Const (uri,exp_named_subst) ->
       incr fdebug ;
-      check_exp_named_subst context exp_named_subst ;
+      check_exp_named_subst ~subst context exp_named_subst ;
       let cty =
        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
       in
@@ -1438,7 +1456,7 @@ and type_of_aux' metasenv context t =
        cty
    | C.MutInd (uri,i,exp_named_subst) ->
       incr fdebug ;
-      check_exp_named_subst context exp_named_subst ;
+      check_exp_named_subst ~subst context exp_named_subst ;
       let cty =
        CicSubstitution.subst_vars exp_named_subst
         (type_of_mutual_inductive_defs uri i)
@@ -1446,7 +1464,7 @@ and type_of_aux' metasenv context t =
        decr fdebug ;
        cty
    | C.MutConstruct (uri,i,j,exp_named_subst) ->
-      check_exp_named_subst context exp_named_subst ;
+      check_exp_named_subst ~subst context exp_named_subst ;
       let cty =
        CicSubstitution.subst_vars exp_named_subst
         (type_of_mutual_inductive_constr uri i j)
@@ -1455,219 +1473,212 @@ and type_of_aux' metasenv context t =
    | C.MutCase (uri,i,outtype,term,pl) ->
       let outsort = type_of_aux context outtype in
       let (need_dummy, k) =
-       let rec guess_args context t =
-         let outtype = CicReduction.whd context t in
-         match outtype with
-           C.Sort _ -> (true, 0)
-         | C.Prod (name, s, t) ->
-            let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
-             if n = 0 then
-              (* last prod before sort *)
-              match CicReduction.whd context s with
+      let rec guess_args context t =
+        let outtype = CicReduction.whd ~subst context t in
+          match outtype with
+              C.Sort _ -> (true, 0)
+            | C.Prod (name, s, t) ->
+		let (b, n) = 
+		  guess_args ((Some (name,(C.Decl s)))::context) t in
+		  if n = 0 then
+		  (* last prod before sort *)
+		    match CicReduction.whd ~subst context s with
 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
-                 C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
-                  (false, 1)
+			C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
+			  (false, 1)
 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
-               | C.Appl ((C.MutInd (uri',i',_)) :: _)
-                  when U.eq uri' uri && i' = i -> (false, 1)
-               | _ -> (true, 1)
-             else
-              (b, n + 1)
-         | _ ->
-             raise (TypeCheckerFailure (sprintf
-              "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
-       in
-        (*CSC whd non serve dopo type_of_aux ? *)
-        let (b, k) = guess_args context outsort in
-         if not b then (b, k - 1) else (b, k)
+		      | C.Appl ((C.MutInd (uri',i',_)) :: _)
+			  when U.eq uri' uri && i' = i -> (false, 1)
+		      | _ -> (true, 1)
+		  else
+		    (b, n + 1)
+            | _ ->
+		raise 
+		  (TypeCheckerFailure 
+		     (sprintf
+			"Malformed case analasys' output type %s" 
+			(CicPp.ppterm outtype)))
       in
+      let (b, k) = guess_args context outsort in
+      if not b then (b, k - 1) else (b, k) in
       let (parameters, arguments, exp_named_subst) =
-        match R.whd context (type_of_aux context term) with
-           (*CSC manca il caso dei CAST *)
-(*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
-(*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
-(*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
-           C.MutInd (uri',i',exp_named_subst) as typ ->
-            if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
-            else raise (TypeCheckerFailure (sprintf
-              "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
-              (CicPp.ppterm typ) (U.string_of_uri uri) i))
-         | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
-            if U.eq uri uri' && i = i' then
-             let params,args =
-              split tl (List.length tl - k)
-             in params,args,exp_named_subst
-            else raise (TypeCheckerFailure (sprintf
-              "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
-              (CicPp.ppterm typ') (U.string_of_uri uri) i))
-         | _ ->
-             raise (TypeCheckerFailure (sprintf
-               "Case analysis: analysed term %s is not an inductive one"
-                (CicPp.ppterm term)))
+        match R.whd ~subst context (type_of_aux context term) with
+            C.MutInd (uri',i',exp_named_subst) as typ ->
+              if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
+              else raise 
+		(TypeCheckerFailure 
+		   (sprintf
+		      "Case analysys: analysed term type is %s, 
+                        but is expected to be (an application of) %s#1/%d{_}"
+		      (CicPp.ppterm typ) (U.string_of_uri uri) i))
+          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+              if U.eq uri uri' && i = i' then
+		let params,args =
+		  split tl (List.length tl - k)
+		in params,args,exp_named_subst
+              else raise 
+		(TypeCheckerFailure 
+		   (sprintf
+		      "Case analysys: analysed term type is %s, 
+                       but is expected to be (an application of) %s#1/%d{_}"
+		      (CicPp.ppterm typ') (U.string_of_uri uri) i))
+          | _ ->
+              raise 
+		(TypeCheckerFailure 
+		   (sprintf
+		      "Case analysis: analysed term %s is not an inductive one"
+                      (CicPp.ppterm term)))
       in
-       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
-       let sort_of_ind_type =
+	(* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
+      let sort_of_ind_type =
         if parameters = [] then
-         C.MutInd (uri,i,exp_named_subst)
+          C.MutInd (uri,i,exp_named_subst)
         else
-         C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
-       in
-        if not (check_allowed_sort_elimination context uri i need_dummy
-         sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
-        then
-         raise
+          C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters) in
+      if not 
+	(check_allowed_sort_elimination context uri i need_dummy
+	   sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
+      then
+        raise
           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
         (* let's check if the type of branches are right *)
-        let parsno =
-         match CicEnvironment.get_cooked_obj ~trust:false uri with
+      let parsno =
+        match CicEnvironment.get_cooked_obj ~trust:false uri with
             C.InductiveDefinition (_,_,parsno) -> parsno
           | _ ->
               raise (TypeCheckerFailure
                 ("Unknown mutual inductive definition:" ^
-                UriManager.string_of_uri uri))
-        in
-         let (_,branches_ok) =
-          List.fold_left
-           (fun (j,b) p ->
+                  UriManager.string_of_uri uri))
+      in
+      let (_,branches_ok) =
+        List.fold_left
+          (fun (j,b) p ->
              let cons =
-              if parameters = [] then
-               (C.MutConstruct (uri,i,j,exp_named_subst))
-              else
-               (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
-             in
-(*
-              (j + 1, b &&
-*)
-              (j + 1,
-let res = b &&
-               R.are_convertible context (type_of_aux context p)
-                (type_of_branch context parsno need_dummy outtype cons
-                  (type_of_aux context cons))
-in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
-              )
-           ) (1,true) pl
-         in
-          if not branches_ok then
-           raise
-            (TypeCheckerFailure "Case analysys: wrong branch type");
-          if not need_dummy then
-           C.Appl ((outtype::arguments)@[term])
-          else if arguments = [] then
-           outtype
-          else
-           C.Appl (outtype::arguments)
+               if parameters = [] then
+		 (C.MutConstruct (uri,i,j,exp_named_subst))
+               else
+		 (C.Appl 
+		    (C.MutConstruct (uri,i,j,exp_named_subst)::parameters)) in
+               (j + 1,
+		  let res = 
+		    b &&
+	            R.are_convertible 
+	              ~subst ~metasenv context (type_of_aux context p)
+	              (type_of_branch context parsno need_dummy outtype cons
+			 (type_of_aux context cons)) in 
+		    if not res then 
+		      debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
+               )
+          ) (1,true) pl
+      in
+      if not branches_ok then
+        raise
+          (TypeCheckerFailure "Case analysys: wrong branch type");
+      if not need_dummy then
+        C.Appl ((outtype::arguments)@[term])
+      else if arguments = [] then
+        outtype
+      else
+        C.Appl (outtype::arguments)
    | C.Fix (i,fl) ->
-      let types_times_kl =
+       let types_times_kl =
        List.rev
-        (List.map
-          (fun (n,k,ty,_) ->
-            let _ = type_of_aux context ty in
-             (Some (C.Name n,(C.Decl ty)),k)) fl)
-      in
-      let (types,kl) = List.split types_times_kl in
+         (List.map
+            (fun (n,k,ty,_) ->
+               let _ = type_of_aux context ty in
+		 (Some (C.Name n,(C.Decl ty)),k)) fl)
+       in
+       let (types,kl) = List.split types_times_kl in
        let len = List.length types in
-        List.iter
-         (fun (name,x,ty,bo) ->
-           if
-            (R.are_convertible (types@context) (type_of_aux (types@context) bo)
-             (CicSubstitution.lift len ty))
-           then
-            begin
-             let (m, eaten, context') =
-              eat_lambdas (types @ context) (x + 1) bo
-             in
-              (*let's control the guarded by destructors conditions D{f,k,x,M}*)
+         List.iter
+           (fun (name,x,ty,bo) ->
               if
-               not
-                (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
+		(R.are_convertible 
+		   ~subst ~metasenv (types@context) (type_of_aux (types@context) bo)
+		   (CicSubstitution.lift len ty))
               then
-               raise
-                (TypeCheckerFailure ("Fix: not guarded by destructors"))
-            end
-           else
-            raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
-         ) fl ;
-      
+	      begin
+		let (m, eaten, context') =
+		  eat_lambdas ~subst (types @ context) (x + 1) bo in
+		  (*let's control the guarded by destructors conditions D{f,k,x,M}*)
+		if
+		  not (guarded_by_destructors context' 
+			 eaten (len + eaten) kl 1 [] m)
+                then
+		  raise
+                    (TypeCheckerFailure ("Fix: not guarded by destructors"))
+              end
+              else
+		raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
+           ) fl ;
         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
-        let (_,_,ty,_) = List.nth fl i in
-        ty
+         let (_,_,ty,_) = List.nth fl i in
+         ty
    | C.CoFix (i,fl) ->
-      let types =
+       let types =
        List.rev
         (List.map
           (fun (n,ty,_) -> 
             let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
-      in
+       in
        let len = List.length types in
-        List.iter
+       List.iter
          (fun (_,ty,bo) ->
-           if
-            (R.are_convertible (types @ context)
-             (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
-           then
-            begin
-             (* let's control that the returned type is coinductive *)
-             match returns_a_coinductive context ty with
-                None ->
-                 raise
-                  (TypeCheckerFailure
-                    ("CoFix: does not return a coinductive type"))
-              | Some uri ->
-                 (*let's control the guarded by constructors conditions C{f,M}*)
-                 if
-                  not
-                   (guarded_by_constructors (types @ context) 0 len false bo
-                     [] uri)
-                 then
-                  raise
-                   (TypeCheckerFailure ("CoFix: not guarded by constructors"))
-            end
-           else
-            raise
-             (TypeCheckerFailure ("CoFix: ill-typed bodies"))
+            if
+              (R.are_convertible 
+		 ~subst ~metasenv (types @ context)
+		 (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
+            then
+              begin
+	      (* let's control that the returned type is coinductive *)
+              match returns_a_coinductive context ty with
+                  None ->
+                    raise
+                    (TypeCheckerFailure
+                       ("CoFix: does not return a coinductive type"))
+		| Some uri ->
+                    (*let's control the guarded by constructors conditions C{f,M}*)
+                    if
+                      not
+			(guarded_by_constructors 
+			   (types @ context) 0 len false bo [] uri)
+                    then
+                      raise
+			(TypeCheckerFailure ("CoFix: not guarded by constructors"))
+              end
+            else
+              raise
+		(TypeCheckerFailure ("CoFix: ill-typed bodies"))
          ) fl ;
-      
-        let (_,ty,_) = List.nth fl i in
+         let (_,ty,_) = List.nth fl i in
          ty
 
- and check_exp_named_subst context =
-  let rec check_exp_named_subst_aux substs =
+ and check_exp_named_subst ?(subst = []) context =
+  let rec check_exp_named_subst_aux esubsts =
    function
       [] -> ()
-    | ((uri,t) as subst)::tl ->
+    | ((uri,t) as item)::tl ->
        let typeofvar =
-        CicSubstitution.subst_vars substs (type_of_variable uri) in
-(* CSC: this test should not exist
-       (match CicEnvironment.get_cooked_obj ~trust:false uri with
-           Cic.Variable (_,Some bo,_,_) ->
-            raise
-             (TypeCheckerFailure
-               ("A variable with a body can not be explicit substituted"))
-         | Cic.Variable (_,None,_,_) -> ()
-         | _ ->
-            raise (TypeCheckerFailure
-              ("Unknown variable definition:" ^
-              UriManager.string_of_uri uri))
-       ) ;
-*)
+	 CicSubstitution.subst_vars esubsts (type_of_variable uri) in
        let typeoft = type_of_aux context t in
-        if CicReduction.are_convertible context typeoft typeofvar then
-         check_exp_named_subst_aux (substs@[subst]) tl
-        else
+       if CicReduction.are_convertible 
+	 ~subst ~metasenv context typeoft typeofvar then
+         check_exp_named_subst_aux (esubsts@[item]) tl
+       else
          begin
-          CicReduction.fdebug := 0 ;
-          ignore (CicReduction.are_convertible context typeoft typeofvar) ;
-          fdebug := 0 ;
-          debug typeoft [typeofvar] ;
-          raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
+           CicReduction.fdebug := 0 ;
+           ignore (CicReduction.are_convertible ~subst ~metasenv context typeoft typeofvar) ;
+           fdebug := 0 ;
+           debug typeoft [typeofvar] ;
+           raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
          end
   in
    check_exp_named_subst_aux []
 
- and sort_of_prod context (name,s) (t1, t2) =
+ and sort_of_prod ?(subst = []) context (name,s) (t1, t2) =
   let module C = Cic in
-   let t1' = CicReduction.whd context t1 in
-   let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
+   let t1' = CicReduction.whd ~subst context t1 in
+   let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
    match (t1', t2') with
       (C.Sort s1, C.Sort s2)
         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> 
@@ -1690,22 +1701,22 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^
         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
           (CicPp.ppterm t2')))
 
- and eat_prods context hetype =
+ and eat_prods ?(subst = []) context hetype =
   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
   (*CSC: cucinati                                                         *)
   function
      [] -> hetype
    | (hete, hety)::tl ->
-    (match (CicReduction.whd context hetype) with
+    (match (CicReduction.whd ~subst context hetype) with
         Cic.Prod (n,s,t) ->
-         if CicReduction.are_convertible context hety s then
+         if CicReduction.are_convertible ~subst ~metasenv context hety s then
           (CicReduction.fdebug := -1 ;
-           eat_prods context (CicSubstitution.subst hete t) tl
+           eat_prods ~subst context (CicSubstitution.subst hete t) tl
           )
          else
           begin
            CicReduction.fdebug := 0 ;
-           ignore (CicReduction.are_convertible context s hety) ;
+           ignore (CicReduction.are_convertible ~subst ~metasenv context s hety) ;
            fdebug := 0 ;
            debug s [hety] ;
            raise (TypeCheckerFailure (sprintf
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 3973c16c1..5f7e3ae97 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -33,7 +33,7 @@ val typecheck : UriManager.uri -> Cic.obj
 
 (* type_of_aux' metasenv context term *)
 val type_of_aux':
- Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
+ ?subst:Cic.substitution -> Cic.metasenv -> Cic.context -> Cic.term -> Cic.term
 
 (* typecheck_mutual_inductive_defs uri (itl,params,indparamsno) *)
 val typecheck_mutual_inductive_defs :
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 387c747f6..b594e009e 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2004, HELM Team.
+(* Copyright (C) 2003, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -80,6 +80,77 @@ let lookup_subst n subst =
     List.assoc n subst
   with Not_found -> raise (SubstNotFound n)
 
+(* clean_up_meta take a metasenv and a term and make every local context
+of each occurrence of a metavariable consistent with its canonical context, 
+with respect to the hidden hipothesis *)
+(*
+let clean_up_meta subst metasenv t =
+  let module C = Cic in
+  let rec aux t =
+  match t with
+      C.Rel _
+    | C.Sort _  -> t
+    | C.Implicit _ -> assert false
+    | C.Meta (n,l) as t ->
+        let cc =
+	  (try
+	     let (cc,_) = lookup_subst n subst in cc
+	   with SubstNotFound _ ->
+	     try
+	       let (_,cc,_) = CicUtil.lookup_meta n metasenv in cc
+             with CicUtil.Meta_not_found _ -> assert false) in
+	let l' = 
+          (try 
+	     List.map2
+	       (fun t1 t2 ->
+		  match t1,t2 with 
+		      None , _ -> None
+		    | _ , t -> t) cc l
+	   with 
+	       Invalid_argument _ -> assert false) in
+        C.Meta (n, l')
+    | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+    | C.Prod (name,so,dest) -> C.Prod (name, aux so, aux dest)
+    | C.Lambda (name,so,dest) -> C.Lambda (name, aux so, aux dest)
+    | C.LetIn (name,so,dest) -> C.LetIn (name, aux so, aux dest)
+    | C.Appl l -> C.Appl (List.map aux l)
+    | C.Var (uri,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+        in
+        C.Var (uri, exp_named_subst')
+    | C.Const (uri, exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+        in
+        C.Const (uri, exp_named_subst')
+    | C.MutInd (uri,tyno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+        in
+        C.MutInd (uri, tyno, exp_named_subst')
+    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+        let exp_named_subst' =
+          List.map (fun (uri,t) -> (uri, aux t)) exp_named_subst
+        in
+        C.MutConstruct (uri, tyno, consno, exp_named_subst')
+    | C.MutCase (uri,tyno,out,te,pl) ->
+        C.MutCase (uri, tyno, aux out, aux te, List.map aux pl)
+    | C.Fix (i,fl) ->
+       let fl' =
+         List.map
+          (fun (name,j,ty,bo) -> (name, j, aux ty, aux bo)) fl
+       in
+       C.Fix (i, fl')
+    | C.CoFix (i,fl) ->
+       let fl' =
+         List.map
+          (fun (name,ty,bo) -> (name, aux ty, aux bo)) fl
+       in
+       C.CoFix (i, fl')
+ in
+ aux t *)
+
 (*** Functions to apply a substitution ***)
 
 let apply_subst_gen ~appl_fun subst term =
@@ -219,14 +290,6 @@ let apply_subst_metasenv subst metasenv =
 
 (***** Pretty printing functions ******)
 
-let ppsubst subst =
-  String.concat "\n"
-    (List.map
-      (fun (idx, (_, term)) ->
-        Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
-      subst)
-;;
-
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppterm_in_context subst term name_context =
@@ -250,6 +313,29 @@ let ppcontext' ?(sep = "\n") subst context =
           sprintf "%s_ :? _" (separate i), None::name_context
     ) context ("",[])
 
+let ppsubst_unfolded subst =
+  String.concat "\n"
+    (List.map
+      (fun (idx, (c, t)) ->
+        let context,name_context = ppcontext' ~sep:"; " subst c in
+         sprintf "%s |- ?%d:= %s" context idx
+          (ppterm_in_context subst t name_context))
+       subst)
+(* 
+        Printf.sprintf "?%d := %s" idx (CicPp.ppterm term))
+      subst) *)
+;;
+
+let ppsubst subst =
+  String.concat "\n"
+    (List.map
+      (fun (idx, (c, t)) ->
+        let context,name_context = ppcontext' ~sep:"; " [] c in
+         sprintf "%s |- ?%d:= %s" context idx
+          (ppterm_in_context [] t name_context))
+       subst)
+;;
+
 let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context)
 
 let ppmetasenv ?(sep = "\n") metasenv subst =
@@ -307,6 +393,7 @@ let tempi_type_of_aux = ref 0.0;;
   (* assumption: metasenv is already instantiated wrt subst *)
 let type_of_aux' metasenv subst context term =
   let time1 = Unix.gettimeofday () in
+(* let term = clean_up_meta subst metasenv term in *)
   let term = apply_subst subst term in
   let context = apply_subst_context subst context in
 (*   let metasenv = apply_subst_metasenv subst metasenv in *)
@@ -431,7 +518,7 @@ let rec restrict subst to_be_restricted metasenv =
       (List.map
         (fun i ->
           try
-           match List.nth context i with
+           match List.nth context (i-1) with
            | None -> assert false
            | Some (n, _) -> CicPp.ppname n
           with
@@ -512,12 +599,12 @@ let rec restrict subst to_be_restricted metasenv =
         with Occur ->
           raise (MetaSubstFailure (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
-            n (names_of_context_indexes context to_be_restricted))))
+	    n (names_of_context_indexes context to_be_restricted)))) 
       metasenv ([], [])
   in
   let (more_to_be_restricted', subst) = (* restrict subst *)
     List.fold_right
-      (fun (n, (context, term)) (more, subst) ->
+      (fun (n, (context, term)) (more, subst') ->
         let to_be_restricted =
           List.map snd (List.filter (fun (m, _) -> m = n) to_be_restricted)
         in
@@ -532,14 +619,21 @@ let rec restrict subst to_be_restricted metasenv =
           let more_to_be_restricted', term' =
             force_does_not_occur subst restricted term
           in
-          let subst' = (n, (context', term')) :: subst in
+          let subst' = (n, (context', term')) :: subst' in
           let more = more @ more_to_be_restricted @ more_to_be_restricted' in
           (more, subst')
         with Occur ->
-          raise (MetaSubstFailure (sprintf
+          let error_msg = sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
             n (names_of_context_indexes context to_be_restricted) n
-            (ppterm subst term)))))
+            (ppterm subst term)
+	  in
+          (* DEBUG
+          prerr_endline error_msg;
+          prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst));
+          prerr_endline ("subst = \n" ^ (ppsubst subst)); 
+          prerr_endline ("context = \n" ^ (ppcontext subst context)); *)
+          raise (MetaSubstFailure error_msg))) 
       subst ([], [])
   in
   match more_to_be_restricted @ more_to_be_restricted' with
@@ -547,8 +641,16 @@ let rec restrict subst to_be_restricted metasenv =
   | l -> restrict subst l metasenv
 ;;
 
-(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
+(*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*)
+
 let delift n subst context metasenv l t =
+(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
+   otherwise the occur check does not make sense *)
+(*
+ prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto
+ al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); 
+*)
+
  let module S = CicSubstitution in
   let l =
    let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
@@ -587,11 +689,13 @@ let delift n subst context metasenv l t =
         in
          C.Var (uri,exp_named_subst')
      | C.Meta (i, l1) as t -> 
-        if i = n then
+         (* see the top level invariant *)
+	 if (i = n) then 
           raise (MetaSubstFailure (sprintf
             "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)"
-            i (ppterm subst t)))
+            i (ppterm subst t))) 
         else
+         begin
          (* I do not consider the term associated to ?i in subst since *)
          (* in this way I can restrict if something goes wrong.        *)
           let rec deliftl j =
@@ -605,10 +709,11 @@ let delift n subst context metasenv l t =
                 with
                    NotInTheList
                  | MetaSubstFailure _ ->
-                    to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
+		     to_be_restricted := (i,j)::!to_be_restricted ; None::l1'
           in
-           let l' = deliftl 1 l1 in
-            C.Meta(i,l')
+            let l' = deliftl 1 l1 in
+              C.Meta(i,l')
+	 end
      | C.Sort _ as t -> t
      | C.Implicit _ as t -> t
      | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty)
@@ -661,7 +766,14 @@ let delift n subst context metasenv l t =
       (* The reason is that our delift function is weaker than first  *)
       (* order (in the sense of alpha-conversion). See comment above  *)
       (* related to the delift function.                              *)
-debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ;
+(* debug_print "First Order UnificationFailure during delift" ;
+prerr_endline(sprintf
+        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
+        (ppterm subst t)
+        (String.concat "; "
+          (List.map
+            (function Some t -> ppterm subst t | None -> "_") l
+          ))); *)
       raise (Uncertain (sprintf
         "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
         (ppterm subst t)
diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli
index 14d6da3f6..6ebd5a5b9 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.mli
+++ b/helm/ocaml/cic_unification/cicMetaSubst.mli
@@ -31,7 +31,7 @@ exception SubstNotFound of int
 
 (* The entry (i,t) in a substitution means that *)
 (* (META i) have been instantiated with t.      *)
-type substitution = (int * (Cic.context * Cic.term)) list
+type substitution = (int * (Cic.context * Cic.term)) list 
 
   (** @raise SubstNotFound *)
 val lookup_subst: int -> substitution -> Cic.context * Cic.term
@@ -66,9 +66,12 @@ val delift :
   int -> substitution -> Cic.context -> Cic.metasenv ->
   (Cic.term option) list -> Cic.term ->
     Cic.term * Cic.metasenv * substitution
-
+val restrict :
+  substitution -> (int * int) list -> Cic.metasenv -> 
+  Cic.metasenv * substitution 
 (** {2 Pretty printers} *)
 
+val ppsubst_unfolded: substitution -> string
 val ppsubst: substitution -> string
 val ppterm: substitution -> Cic.term -> string
 val ppcontext: ?sep: string -> substitution -> Cic.context -> string
@@ -92,3 +95,6 @@ val print_counters: unit -> unit
 val reset_counters: unit -> unit
 *)
 
+(* val clean_up_meta :
+  substitution -> Cic.metasenv -> Cic.term -> Cic.term
+*)
diff --git a/helm/ocaml/cic_unification/cicMkImplicit.ml b/helm/ocaml/cic_unification/cicMkImplicit.ml
index 748307013..b6aa1df41 100644
--- a/helm/ocaml/cic_unification/cicMkImplicit.ml
+++ b/helm/ocaml/cic_unification/cicMkImplicit.ml
@@ -51,6 +51,10 @@ let new_meta metasenv subst =
   in
   1 + aux (None, indexes)
 
+(* let apply_subst_context = CicMetaSubst.apply_subst_context;; *)
+(* questa o la precedente sembrano essere equivalenti come tempi *)
+let apply_subst_context _ context = context ;;
+
 let mk_implicit metasenv subst context =
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
@@ -58,7 +62,7 @@ let mk_implicit metasenv subst context =
     (* in the following mk_* functions we apply substitution to canonical
     * context since we have the invariant that the metasenv has already been
     * instantiated with subst *)
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv) ;
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []);
@@ -68,7 +72,7 @@ let mk_implicit metasenv subst context =
 let mk_implicit_type metasenv subst context =
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   ([ newmeta, [], Cic.Sort (Cic.Type newuniv);
     (* TASSI: ?? *)
     newmeta + 1, context, Cic.Meta (newmeta, []) ] @metasenv,
@@ -84,7 +88,7 @@ let n_fresh_metas metasenv subst context n =
   if n = 0 then metasenv, []
   else 
     let irl = identity_relocation_list_for_metavariable context in
-    let context = CicMetaSubst.apply_subst_context subst context in
+    let context = apply_subst_context subst context in
     let newmeta = new_meta metasenv subst in
     let newuniv = CicUniv.fresh () in
     let rec aux newmeta n = 
@@ -100,7 +104,7 @@ let n_fresh_metas metasenv subst context n =
       
 let fresh_subst metasenv subst context uris = 
   let irl = identity_relocation_list_for_metavariable context in
-  let context = CicMetaSubst.apply_subst_context subst context in
+  let context = apply_subst_context subst context in
   let newmeta = new_meta metasenv subst in
   let newuniv = CicUniv.fresh () in
   let rec aux newmeta = function
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index c1b70df8d..7b3e4179c 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -107,8 +107,9 @@ and type_of_mutual_inductive_constr uri i j =
  
 and check_branch n context metasenv subst left_args_no actualtype term expectedtype =
   let module C = Cic in
-  let module R = CicMetaSubst in
-  match R.whd subst context expectedtype with
+  (* let module R = CicMetaSubst in *)
+  let module R = CicReduction in
+  match R.whd ~subst context expectedtype with
      C.MutInd (_,_,_) ->
        (n,context,actualtype, [term]), subst, metasenv
    | C.Appl (C.MutInd (_,_,_)::tl) ->
@@ -117,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
    | C.Prod (name,so,de) ->
       (* we expect that the actual type of the branch has the due 
          number of Prod *)
-      (match R.whd subst context actualtype with
+      (match R.whd ~subst context actualtype with
            C.Prod (name',so',de') ->
              let subst, metasenv = 
                fo_unif_subst subst context metasenv so so' in
@@ -158,13 +159,13 @@ and type_of_aux' metasenv context t =
        ty,subst',metasenv'
     | C.Meta (n,l) -> 
         (try
-          let (canonical_context, term) = CicMetaSubst.lookup_subst n subst in
+          let (canonical_context, term) = CicUtil.lookup_subst n subst in
           let subst,metasenv =
             check_metasenv_consistency n subst metasenv context
               canonical_context l
           in
           type_of_aux subst metasenv context (CicSubstitution.lift_meta l term)
-        with CicMetaSubst.SubstNotFound _ ->
+        with CicUtil.Subst_not_found _ ->
           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
           let subst,metasenv =
             check_metasenv_consistency n subst metasenv context
@@ -202,7 +203,7 @@ and type_of_aux' metasenv context t =
         sort_of_prod subst'' metasenv'' context (name,s) (sort1,sort2)
    | C.Lambda (n,s,t) ->
        let sort1,subst',metasenv' = type_of_aux subst metasenv context s in
-       (match CicMetaSubst.whd subst' context sort1 with
+       (match CicReduction.whd ~subst:subst' context sort1 with
            C.Meta _
          | C.Sort _ -> ()
          | _ ->
@@ -271,7 +272,7 @@ and type_of_aux' metasenv context t =
              (RefineFailure
               ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in
        let rec count_prod t =
-         match CicMetaSubst.whd subst context t with
+         match CicReduction.whd ~subst context t with
              C.Prod (_, _, t) -> 1 + (count_prod t)
            | _ -> 0 in 
        let no_args = count_prod arity in
@@ -296,7 +297,7 @@ and type_of_aux' metasenv context t =
        let _, subst, metasenv =
          type_of_aux subst metasenv context expected_type
        in
-       let actual_type = CicMetaSubst.whd subst context actual_type in
+       let actual_type = CicReduction.whd ~subst context actual_type in
        let subst,metasenv =
          fo_unif_subst subst context metasenv expected_type actual_type
        in
@@ -347,11 +348,21 @@ and type_of_aux' metasenv context t =
                   type_of_aux subst metasenv context appl
                 in
 *)
-                CicMetaSubst.whd subst context appl
+                (* DEBUG 
+                let prova1 = CicMetaSubst.whd subst context appl in
+                let prova2 = CicReduction.whd ~subst context appl in
+                if not (prova1 = prova2) then
+                  begin 
+		    prerr_endline ("prova1 =" ^ (CicPp.ppterm prova1));
+		    prerr_endline ("prova2 =" ^ (CicPp.ppterm prova2));
+                  end;
+                *)
+                (* CicMetaSubst.whd subst context appl *)
+                CicReduction.whd ~subst context appl
               in
                fo_unif_subst subst context metasenv instance instance')
              (subst,metasenv) outtypeinstances in
-        CicMetaSubst.whd subst
+        CicReduction.whd ~subst
           context (C.Appl(outtype::right_args@[term])),subst,metasenv
    | C.Fix (i,fl) ->
       let subst,metasenv,types =
@@ -370,7 +381,7 @@ and type_of_aux' metasenv context t =
             type_of_aux subst metasenv context' bo
            in
             fo_unif_subst subst context' metasenv
-              ty_of_bo (CicMetaSubst.lift subst len ty)
+              ty_of_bo (CicSubstitution.lift len ty)
          ) (subst,metasenv) fl in
         let (_,_,ty,_) = List.nth fl i in
          ty,subst,metasenv
@@ -391,7 +402,7 @@ and type_of_aux' metasenv context t =
             type_of_aux subst metasenv context' bo
            in
             fo_unif_subst subst context' metasenv
-              ty_of_bo (CicMetaSubst.lift subst len ty)
+              ty_of_bo (CicSubstitution.lift len ty)
          ) (subst,metasenv) fl in
       
         let (_,ty,_) = List.nth fl i in
@@ -420,7 +431,7 @@ and type_of_aux' metasenv context t =
             C.Def ((S.lift_meta l (S.lift i t)),
               Some (S.lift_meta l (S.lift i ty))))) :: (aux (i+1) tl)
      in
-      aux 1 canonical_context
+      aux 1 canonical_context 
     in
     try
      List.fold_left2 
@@ -493,8 +504,8 @@ and type_of_aux' metasenv context t =
  and sort_of_prod subst metasenv context (name,s) (t1, t2) =
   let module C = Cic in
     let context_for_t2 = (Some (name,C.Decl s))::context in
-    let t1'' = CicMetaSubst.whd subst context t1 in
-    let t2'' = CicMetaSubst.whd subst context_for_t2 t2 in
+    let t1'' = CicReduction.whd ~subst context t1 in
+    let t2'' = CicReduction.whd ~subst context_for_t2 t2 in
     match (t1'', t2'') with
        (C.Sort s1, C.Sort s2)
          when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different than Coq manual!!! *)
@@ -548,21 +559,22 @@ and type_of_aux' metasenv context t =
         (* Thus I generate a name (name_hint) in context and   *)
         (* then I generate a name --- using the hint name_hint *)
         (* --- that is fresh in (context'@context).            *)
-        let name_hint =
-         FreshNamesGenerator.mk_fresh_name metasenv
+        let name_hint = 
+	  (* Cic.Name "pippo" *)
+         FreshNamesGenerator.mk_fresh_name metasenv 
 (*           (CicMetaSubst.apply_subst_metasenv subst metasenv) *)
           (CicMetaSubst.apply_subst_context subst context)
           Cic.Anonymous
-          (CicMetaSubst.apply_subst subst argty)
+          (CicMetaSubst.apply_subst subst argty) 
         in
          (* [] and (Cic.Sort Cic.prop) are dummy: they will not be used *)
          FreshNamesGenerator.mk_fresh_name
           [] context name_hint (Cic.Sort Cic.Prop)
        in
        let metasenv,target =
-        mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
+         mk_prod metasenv ((Some (name, Cic.Decl meta))::context) tl
        in
-        metasenv,Cic.Prod (name,meta,target)
+         metasenv,Cic.Prod (name,meta,target)
  in
   let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in
   let (subst, metasenv) =
@@ -575,10 +587,31 @@ and type_of_aux' metasenv context t =
         (match hetype with
             Cic.Prod (n,s,t) ->
               let subst,metasenv =
-               fo_unif_subst subst context metasenv hety s
+                fo_unif_subst subst context metasenv hety s
+(*
+               try 
+		 fo_unif_subst subst context metasenv hety s
+	       with _ ->
+                 prerr_endline("senza subst fallisce");
+                 let hety = CicMetaSubst.apply_subst subst hety in
+                 let s = CicMetaSubst.apply_subst subst s in
+		 prerr_endline ("unifico = " ^(CicPp.ppterm hety));
+		 prerr_endline ("con = " ^(CicPp.ppterm s));
+		 fo_unif_subst subst context metasenv hety s *)
               in
-               eat_prods metasenv subst context
-                (CicMetaSubst.subst subst hete t) tl
+              (* DEBUG 
+              let t1 = CicMetaSubst.subst subst hete t in
+	      let t2 = CicSubstitution.subst hete t in
+		prerr_endline ("con subst = " ^(CicPp.ppterm t1));
+		prerr_endline ("senza subst = " ^(CicPp.ppterm t2));
+                prerr_endline("++++++++++metasenv prima di eat_prods:\n" ^
+			       (CicMetaSubst.ppmetasenv metasenv subst));
+                prerr_endline("++++++++++subst prima di eat_prods:\n" ^
+			       (CicMetaSubst.ppsubst subst));
+              *)
+	      eat_prods metasenv subst context
+                (* (CicMetaSubst.subst subst hete t) tl *)
+                (CicSubstitution.subst hete t) tl 
           | _ -> assert false
         )
    in
@@ -634,15 +667,20 @@ and type_of_aux' metasenv context t =
   in
    aux [] [] (hetype,subst,metasenv) tlbody_and_type
 *)
- in
+ in 
   let ty,subst',metasenv' =
    type_of_aux [] metasenv context t
   in
    let substituted_t = CicMetaSubst.apply_subst subst' t in
    let substituted_ty = CicMetaSubst.apply_subst subst' ty in
-   let substituted_metasenv = metasenv'
-(*     CicMetaSubst.apply_subst_metasenv subst' metasenv' *)
-   in
+(* Andrea: ho rimesso qui l'applicazione della subst al
+metasenv dopo che ho droppato l'invariante che il metsaenv
+e' sempre istanziato *)
+   let substituted_metasenv = 
+     CicMetaSubst.apply_subst_metasenv subst' metasenv' in
+       (* metasenv' *)
+(*  substituted_t,substituted_ty,substituted_metasenv *)
+(* ANDREA: spostare tutta questa robaccia da un altra parte *)
     let cleaned_t =
      FreshNamesGenerator.clean_dummy_dependent_types substituted_t in
     let cleaned_ty =
@@ -672,20 +710,20 @@ and type_of_aux' metasenv context t =
          (n,context',ty')
       ) substituted_metasenv
     in
-     (cleaned_t,cleaned_ty,cleaned_metasenv)
-
+     (cleaned_t,cleaned_ty,cleaned_metasenv) 
 ;;
 
-(* DEBUGGING ONLY *)
+
+
+(* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try
-  let (t,ty,m) = type_of_aux' metasenv context term in
-   debug_print
-    ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
-(*
+  let (t,ty,m) = 
+      type_of_aux' metasenv context term in
+    debug_print
+     ("@@@ REFINE SUCCESSFUL: " ^ CicPp.ppterm t ^ " : " ^ CicPp.ppterm ty);
    debug_print
-    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv m s);
-*)
+    ("@@@ REFINE SUCCESSFUL (metasenv):\n" ^ CicMetaSubst.ppmetasenv ~sep:";" m []);
    (t,ty,m)
  with
  | RefineFailure msg as e ->
@@ -694,4 +732,4 @@ let type_of_aux' metasenv context term =
  | Uncertain msg as e ->
      debug_print ("@@@ REFINE UNCERTAIN: " ^ msg);
      raise e
-;;
+;; *)
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index e6213d6af..cebbb9e8f 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -32,6 +32,21 @@ exception AssertFailure of string;;
 let debug_print = prerr_endline
 
 let type_of_aux' metasenv subst context term =
+  try 
+    CicTypeChecker.type_of_aux' ~subst metasenv context term
+  with
+      CicTypeChecker.TypeCheckerFailure msg ->
+	let msg =
+	  (sprintf
+	   "Kernel Type checking error: 
+%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad."
+             (CicMetaSubst.ppterm subst term)
+             (CicMetaSubst.ppterm [] term)
+             (CicMetaSubst.ppcontext subst context)
+             (CicMetaSubst.ppmetasenv metasenv subst) 
+             (CicMetaSubst.ppsubst subst) msg) in
+        raise (AssertFailure msg);;
+(*
   try
     CicMetaSubst.type_of_aux' metasenv subst context term
   with
@@ -41,7 +56,19 @@ let type_of_aux' metasenv subst context term =
         "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms"
         (CicMetaSubst.ppterm subst term)
         (CicMetaSubst.ppcontext subst context)
-        (CicMetaSubst.ppmetasenv metasenv subst) msg)))
+        (CicMetaSubst.ppmetasenv metasenv subst) msg))) *)
+
+let rec deref subst =
+  function
+      Cic.Meta(n,l) as t -> 
+	(try 
+	   deref subst
+	     (CicSubstitution.lift_meta 
+		l (snd (CicUtil.lookup_subst n subst))) 
+	 with 
+	   CicUtil.Subst_not_found _ -> t)
+    | t -> t
+;;
 
 let rec beta_expand test_equality_only metasenv subst context t arg =
  let module S = CicSubstitution in
@@ -49,8 +76,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
   let rec aux metasenv subst n context t' =
    try
     let subst,metasenv =
-     fo_unif_subst test_equality_only subst context metasenv
-      (CicSubstitution.lift n arg) t'
+      fo_unif_subst test_equality_only subst context metasenv 
+	(CicSubstitution.lift n arg) t'
     in
      subst,metasenv,C.Rel (1 + n)
    with
@@ -63,24 +90,32 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
             aux_exp_named_subst metasenv subst n context exp_named_subst
            in
             subst,metasenv,C.Var (uri,exp_named_subst')
-        | C.Meta (i,l) as t->
-           (try
-             let (_, t') = CicMetaSubst.lookup_subst i subst in
-              aux metasenv subst n context (CicSubstitution.lift_meta l t')
-            with CicMetaSubst.SubstNotFound _ ->
-              let (subst, metasenv, context, local_context) =
-                List.fold_left
-                  (fun (subst, metasenv, context, local_context) t ->
-                    match t with
+        | C.Meta (i,l) ->
+	    (* andrea: in general, beta_expand can create badly typed
+             terms. This happens quite seldom in practice, UNLESS we
+             iterate on the local context. For this reason, we renounce
+             to iterate and just lift *)
+            let l = 
+	      List.map 
+		(function
+		     Some t -> Some (CicSubstitution.lift 1 t)
+		   | None -> None) l in
+	    subst, metasenv, C.Meta (i,l)
+            (*
+            let (subst, metasenv, context, local_context) =
+              List.fold_right
+                (fun t (subst, metasenv, context, local_context) ->
+                   match t with
                     | None -> (subst, metasenv, context, None :: local_context)
                     | Some t ->
                         let (subst, metasenv, t) =
                           aux metasenv subst n context t
                         in
-                        (subst, metasenv, context, Some t :: local_context))
-                  (subst, metasenv, context, []) l
-              in
-              (subst, metasenv, C.Meta (i, local_context)))
+                          (subst, metasenv, context, Some t :: local_context))
+                l (subst, metasenv, context, [])
+            in
+  prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context))));
+              (subst, metasenv, C.Meta (i, local_context)) *)
         | C.Sort _
         | C.Implicit _ as t -> subst,metasenv,t
         | C.Cast (te,ty) ->
@@ -149,7 +184,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
                fl
             in
              C.Fix (i, substitutedfl)
-*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+*) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *)
+   subst,metasenv,CicSubstitution.lift 1 t' 
         | C.CoFix (i,fl) ->
 (*CSC: not implemented
            let tylen = List.length fl in
@@ -159,7 +195,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
                fl
             in
              C.CoFix (i, substitutedfl)
-*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+*) (* subst,metasenv,CicMetasubst.lift subst 1 t' *)
+    subst,metasenv,CicSubstitution.lift 1 t'
 
   and aux_exp_named_subst metasenv subst n context ens =
    List.fold_right
@@ -173,13 +210,21 @@ let rec beta_expand test_equality_only metasenv subst context t arg =
     metasenv context (Cic.Name "Heta") ~typ:argty
   in
    let subst,metasenv,t' = aux metasenv subst 0 context t in
+ (* prova *)
+ (* old 
     subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
+ *)
+    subst, metasenv, C.Lambda (fresh_name,argty,t')
 
-and beta_expand_many test_equality_only metasenv subst context t =
- List.fold_left
-  (fun (subst,metasenv,t) arg ->
-    beta_expand test_equality_only metasenv subst context t arg
-  ) (subst,metasenv,t)
+and beta_expand_many test_equality_only metasenv subst context t args =
+  let subst,metasenv,hd =
+    List.fold_right
+      (fun arg (subst,metasenv,t) ->
+         let subst,metasenv,t =
+	   beta_expand test_equality_only metasenv subst context t arg in
+         subst,metasenv,t 
+      ) args (subst,metasenv,t) in
+  subst,metasenv,hd
 
 (* NUOVA UNIFICAZIONE *)
 (* A substitution is a (int * Cic.term) list that associates a
@@ -192,45 +237,57 @@ and beta_expand_many test_equality_only metasenv subst context t =
 
 and fo_unif_subst test_equality_only subst context metasenv t1 t2 =  
  let module C = Cic in
- let module R = CicMetaSubst in
+ let module R = CicReduction in
  let module S = CicSubstitution in
+ let t1 = deref subst t1 in
+ let t2 = deref subst t2 in
   match (t1, t2) with
      (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
-       let ok,subst,metasenv =
-       try
-        List.fold_left2
-         (fun (b,subst,metasenv) t1 t2 ->
-           if b then true,subst,metasenv else
-            match t1,t2 with
-               None,_
-             | _,None -> true,subst,metasenv
-             | Some t1', Some t2' ->
-                (* First possibility:  restriction    *)
-                (* Second possibility: unification    *)
-                (* Third possibility:  convertibility *)
-                if R.are_convertible subst context t1' t2' then
-                 true,subst,metasenv
-                else
-                 (try
-                   let subst,metasenv =
-                    fo_unif_subst 
-                     test_equality_only subst context metasenv t1' t2'
-                   in
-                    true,subst,metasenv
-                 with
-                  Not_found -> false,subst,metasenv)
-         ) (true,subst,metasenv) ln lm
-       with
-        Invalid_argument _ ->
-         raise (UnificationFailure (sprintf
-           "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
-       in
-        if ok then
-          subst,metasenv
-        else
-          raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
-            (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+       let _,subst,metasenv =
+	 (try
+            List.fold_left2
+              (fun (j,subst,metasenv) t1 t2 ->
+		 match t1,t2 with
+		     None,_
+		   | _,None -> j+1,subst,metasenv
+		   | Some t1', Some t2' ->
+                       (* First possibility:  restriction    *)
+                       (* Second possibility: unification    *)
+                       (* Third possibility:  convertibility *)
+                       if R.are_convertible ~subst ~metasenv context t1' t2' then
+			 j+1,subst,metasenv
+                       else
+			 (try
+			    let subst,metasenv =
+			      fo_unif_subst 
+				test_equality_only 
+				subst context metasenv t1' t2'
+			    in
+			      j+1,subst,metasenv
+			  with
+			      Uncertain _
+			    | UnificationFailure _ ->
+prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); 
+				let metasenv, subst = 
+				  CicMetaSubst.restrict 
+				    subst [(n,j)] metasenv in
+				  j+1,subst,metasenv)
+	      ) (1,subst,metasenv) ln lm
+	  with
+	      Exit ->
+		raise 
+		(UnificationFailure "1")
+(*
+		   (sprintf
+		      "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
+		      (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
+	    | Invalid_argument _ ->
+		raise 
+		  (UnificationFailure "2"))
+(*
+		     (sprintf
+			"Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))*)
+       in subst,metasenv
    | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
        fo_unif_subst test_equality_only subst context metasenv t2 t1
    | (C.Meta (n,l), t)   
@@ -248,101 +305,88 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
           fo_unif_subst test_equality_only subst context metasenv 
            (lower m1 m2) (upper m1 m2)
        in
-        begin
-        try
-          let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-          let lifted_oldt = S.lift_meta l oldt in
-          let ty_lifted_oldt =
-            type_of_aux' metasenv subst context lifted_oldt
-          in
-          let tyt = type_of_aux' metasenv subst context t in
-          let (subst, metasenv) =
-            fo_unif_subst_ordered test_equality_only subst context metasenv
-              tyt ty_lifted_oldt
-          in
-          fo_unif_subst_ordered 
-            test_equality_only subst context metasenv t lifted_oldt
-        with CicMetaSubst.SubstNotFound _ ->
-         (* First of all we unify the type of the meta with the type of the term *)
+         begin
          let subst,metasenv =
-          let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
-          (try
-            let tyt = type_of_aux' metasenv subst context t in
-             fo_unif_subst 
-              test_equality_only 
-               subst context metasenv tyt (S.lift_meta l meta_type)
-          with AssertFailure _ ->
-            (* TODO huge hack!!!!
-             * we keep on unifying/refining in the hope that the problem will be
-             * eventually solved. In the meantime we're breaking a big invariant:
-             * the terms that we are unifying are no longer well typed in the
-             * current context (in the worst case we could even diverge)
-             *)
-(*
-prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
-prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
-*)
-            (subst, metasenv))
-         in
-          let t',metasenv,subst =
-           try
-            CicMetaSubst.delift n subst context metasenv l t
-           with
-              (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
-            | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
-          in
-           let t'' =
-            match t' with
-               C.Sort (C.Type u) when not test_equality_only ->
-                 let u' = CicUniv.fresh () in
-                 let s = C.Sort (C.Type u') in
-                  ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
-                 s
-              | _ -> t'
-           in
-            (* Unifying the types may have already instantiated n. Let's check *)
-            try
-             let (_, oldt) = CicMetaSubst.lookup_subst n subst in
-             let lifted_oldt = S.lift_meta l oldt in
-              fo_unif_subst_ordered 
-               test_equality_only subst context metasenv t lifted_oldt
-            with
-             CicMetaSubst.SubstNotFound _ -> 
-               let (_, context, _) = CicUtil.lookup_meta n metasenv in
-               let subst = (n, (context, t'')) :: subst in
-               let metasenv =
-(*                 CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
-                CicMetaSubst.apply_subst_metasenv subst metasenv
-               in
-               subst, metasenv
-(*               (n,t'')::subst, metasenv *)
-        end
+           let (_,_,meta_type) =  CicUtil.lookup_meta n metasenv in
+           (try
+              let tyt = type_of_aux' metasenv subst context t in
+		fo_unif_subst 
+		  test_equality_only 
+		  subst context metasenv tyt (S.lift_meta l meta_type)
+            with 
+		UnificationFailure msg 
+	      | Uncertain msg ->
+		  prerr_endline msg;raise (UnificationFailure msg) 
+              | AssertFailure _ ->
+		  prerr_endline "siamo allo huge hack";
+		  (* TODO huge hack!!!!
+		   * we keep on unifying/refining in the hope that 
+		   * the problem will be eventually solved. 
+		   * In the meantime we're breaking a big invariant:
+		   * the terms that we are unifying are no longer well 
+		   * typed in the current context (in the worst case 
+		   * we could even diverge) *)
+		  (subst, metasenv)) in
+	 let t',metasenv,subst =
+	   try 
+	     CicMetaSubst.delift n subst context metasenv l t
+	   with
+	       (CicMetaSubst.MetaSubstFailure msg)-> 
+		 raise (UnificationFailure msg)
+	     | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
+	 in
+	 let t'' =
+	   match t' with
+	       C.Sort (C.Type u) when not test_equality_only ->
+		 let u' = CicUniv.fresh () in
+		 let s = C.Sort (C.Type u') in
+		   ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
+		   s
+	     | _ -> t'
+	 in
+	 (* Unifying the types may have already instantiated n. Let's check *)
+	 try
+	   let (_, oldt) = CicUtil.lookup_subst n subst in
+	   let lifted_oldt = S.lift_meta l oldt in
+	     fo_unif_subst_ordered 
+	       test_equality_only subst context metasenv t lifted_oldt
+	 with
+	     CicUtil.Subst_not_found _ -> 
+	       let (_, context, _) = CicUtil.lookup_meta n metasenv in
+	       let subst = (n, (context, t'')) :: subst in
+	       let metasenv =
+		 List.filter (fun (m,_,_) -> not (n = m)) metasenv in
+	       subst, metasenv
+         end
    | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
    | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
       if UriManager.eq uri1 uri2 then
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2
       else
-       raise (UnificationFailure (sprintf
+       raise (UnificationFailure "3")
+       (* (sprintf
         "Can't unify %s with %s due to different constants"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
    | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 then
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2
       else
-       raise (UnificationFailure (sprintf
+       raise (UnificationFailure "4")
+        (* (sprintf
         "Can't unify %s with %s due to different inductive principles"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
    | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
      C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
       if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
        fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
         exp_named_subst1 exp_named_subst2
       else
-       raise (UnificationFailure (sprintf
+       raise (UnificationFailure "5")
+       (* (sprintf
         "Can't unify %s with %s due to different inductive constructors"
-        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+        (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
    | (C.Implicit _, _) | (_, C.Implicit _) ->  assert false
    | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only 
                               subst context metasenv te t2
@@ -365,31 +409,55 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
        fo_unif_subst 
         test_equality_only subst context metasenv t2 (S.subst s1 t1)
    | (C.Appl l1, C.Appl l2) -> 
-       let subst,metasenv,t1',t2' =
-        match l1,l2 with
-           C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
-             subst,metasenv,t1,t2
-         (* In the first two cases when we reach the next begin ... end
-            section useless work is done since, by construction, the list
-            of arguments will be equal.
-         *)
+       (* andrea: this case should be probably rewritten in the 
+	  spirit of deref *)
+       let rec beta_reduce =
+         function
+             (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+               let he'' = CicSubstitution.subst he' t in
+                 if tl' = [] then
+                   he''
+                 else
+                   beta_reduce (Cic.Appl(he''::tl'))
+           | t -> t in
+        (match l1,l2 with
+           C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j ->
+             (try 
+		List.fold_left2 
+		 (fun (subst,metasenv) ->
+		    fo_unif_subst test_equality_only subst context metasenv)
+		  (subst,metasenv) l1 l2
+	      with (Invalid_argument msg) -> raise (UnificationFailure msg)) 
          | C.Meta (i,l)::args, _ ->
-            let subst,metasenv,t2' =
-             beta_expand_many test_equality_only metasenv subst context t2 args
-            in
-             subst,metasenv,t1,t2'
+            (try 
+	       let (_,t) = CicUtil.lookup_subst i subst in
+	       let lifted = S.lift_meta l t in
+               let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+	       fo_unif_subst 
+		 test_equality_only 
+		 subst context metasenv reduced t2
+	     with CicUtil.Subst_not_found _ ->
+               let subst,metasenv,beta_expanded =
+		 beta_expand_many 
+		   test_equality_only metasenv subst context t2 args in
+               fo_unif_subst test_equality_only subst context metasenv 
+		 (C.Meta (i,l)) beta_expanded) 
          | _, C.Meta (i,l)::args ->
-            let subst,metasenv,t1' =
-             beta_expand_many test_equality_only metasenv subst context t1 args
-            in
-             subst,metasenv,t1',t2
+            (try 
+	       let (_,t) = CicUtil.lookup_subst i subst in
+	       let lifted = S.lift_meta l t in
+               let reduced = beta_reduce (Cic.Appl (lifted::args)) in
+	       fo_unif_subst 
+		 test_equality_only 
+		 subst context metasenv t1 reduced
+	     with CicUtil.Subst_not_found _ ->
+               let subst,metasenv,beta_expanded =
+		 beta_expand_many 
+		   test_equality_only metasenv subst context t1 args in
+               fo_unif_subst test_equality_only subst context metasenv 
+		 (C.Meta (i,l)) beta_expanded)
          | _,_ ->
-             subst,metasenv,t1,t2
-       in
-        begin
-         match t1',t2' with
-            C.Appl l1, C.Appl l2 ->
-             let lr1 = List.rev l1 in
+	     let lr1 = List.rev l1 in
              let lr2 = List.rev l2 in
              let rec fo_unif_l test_equality_only subst metasenv =
               function
@@ -407,9 +475,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
                   in 
                    fo_unif_l test_equality_only subst' metasenv' (l1,l2)
              in
-              fo_unif_l test_equality_only subst metasenv (lr1, lr2) 
-          | _ -> assert false
-        end
+             fo_unif_l test_equality_only subst metasenv (lr1, lr2) )
    | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
        let subst', metasenv' = 
         fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
@@ -422,34 +488,38 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
           ) (subst'',metasenv'') pl1 pl2 
         with
          Invalid_argument _ ->
-          raise (UnificationFailure (sprintf
-            "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))
+          raise (UnificationFailure "6"))
+           (* (sprintf
+            "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *)
    | (C.Rel _, _) | (_,  C.Rel _) ->
        if t1 = t2 then
          subst, metasenv
        else
-        raise (UnificationFailure (sprintf
+        raise (UnificationFailure "6")
+          (* (sprintf
           "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
    | (C.Sort _ ,_) | (_, C.Sort _)
    | (C.Const _, _) | (_, C.Const _)
    | (C.MutInd  _, _) | (_, C.MutInd _)
    | (C.MutConstruct _, _) | (_, C.MutConstruct _)
    | (C.Fix _, _) | (_, C.Fix _) 
    | (C.CoFix _, _) | (_, C.CoFix _) -> 
-       if t1 = t2 || R.are_convertible subst context t1 t2 then
+       if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then
         subst, metasenv
        else
-        raise (UnificationFailure (sprintf
+        raise (UnificationFailure "7")
+        (* (sprintf
           "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
    | (_,_) ->
-       if R.are_convertible subst context t1 t2 then
+       if R.are_convertible ~subst ~metasenv context t1 t2 then
         subst, metasenv
        else
-        raise (UnificationFailure (sprintf
+        raise (UnificationFailure "8")
+         (* (sprintf
           "Can't unify %s with %s because they are not convertible"
-          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))
+          (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *)
 
 and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
  exp_named_subst1 exp_named_subst2
@@ -483,8 +553,8 @@ let fo_unif metasenv context t1 t2 =
  fo_unif_subst false [] context metasenv t1 t2 ;;
 
 let fo_unif_subst subst context metasenv t1 t2 =
-  let enrich_msg msg =
-    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s"
+  let enrich_msg msg = (* "bella roba" *)
+    sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s"
       (CicMetaSubst.ppterm subst t1)
       (try
         CicPp.ppterm (type_of_aux' metasenv subst context t1)
@@ -494,7 +564,8 @@ let fo_unif_subst subst context metasenv t1 t2 =
         CicPp.ppterm (type_of_aux' metasenv subst context t2)
       with _ -> "MALFORMED")
       (CicMetaSubst.ppcontext subst context)
-      (CicMetaSubst.ppmetasenv metasenv subst) msg
+      (CicMetaSubst.ppmetasenv metasenv subst)
+      (CicMetaSubst.ppsubst subst) msg 
   in
   try
     fo_unif_subst false subst context metasenv t1 t2
-- 
2.39.2