From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 5 Sep 2003 10:29:13 +0000 (+0000)
Subject: Defs in context may now have an optional type (when unknown).
X-Git-Tag: v0_0_1~38
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=265cf771fbfe217b5f274b999fc3ad887683a09a;p=helm.git

Defs in context may now have an optional type (when unknown).

During type-checking, LetIn are pushed in the context as Defs with a known
type. When a Rel pointing to a Def in the context is found, the already
computed type (if present) is used instead of re-typing the body of the
LetIn. As a result, we get a (possibly exponential) decrease in the complexity
of the typing algorithm.
---

diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml
index fd46c22b4..6d58e6164 100644
--- a/helm/ocaml/cic/cic.ml
+++ b/helm/ocaml/cic/cic.ml
@@ -171,7 +171,7 @@ and annotation =
 
 and context_entry =                            (* A declaration or definition *)
    Decl of term
- | Def of term
+ | Def of term * term option                   (* body, type (if known) *)
 
 and hypothesis =
  (name * context_entry) option               (* None means no more accessible *)
@@ -185,4 +185,5 @@ and anncontext_entry =                         (* A declaration or definition *)
 and annhypothesis =
  id * (name * anncontext_entry) option       (* None means no more accessible *)
 
-and anncontext = annhypothesis list;;
+and anncontext = annhypothesis list
+;;
diff --git a/helm/ocaml/cic/deannotate.ml b/helm/ocaml/cic/deannotate.ml
index df59305fe..2bee18d6f 100644
--- a/helm/ocaml/cic/deannotate.ml
+++ b/helm/ocaml/cic/deannotate.ml
@@ -108,7 +108,7 @@ let deannotate_obj =
 	     List.map 
 	      (function 
 	          _,Some (n,(C.ADef at)) ->
-                   Some (n,(C.Def (deannotate_term at)))
+                   Some (n,(C.Def ((deannotate_term at),None)))
 	        | _,Some (n,(C.ADecl at)) ->
                    Some (n,(C.Decl (deannotate_term at)))
 	        | _,None -> None
diff --git a/helm/ocaml/cic_omdoc/cic2acic.ml b/helm/ocaml/cic_omdoc/cic2acic.ml
index c0e514d37..4226364fc 100644
--- a/helm/ocaml/cic_omdoc/cic2acic.ml
+++ b/helm/ocaml/cic_omdoc/cic2acic.ml
@@ -23,6 +23,26 @@
  * http://cs.unibo.it/helm/.
  *)
 
+let hashtbl_add_time = ref 0.0;;
+
+let xxx_add h k v =
+ let t1 = Sys.time () in
+  Hashtbl.add h k v ;
+  let t2 = Sys.time () in
+   hashtbl_add_time := !hashtbl_add_time +. t2 -. t1
+;;
+
+let number_new_type_of_aux' = ref 0;;
+let type_of_aux'_add_time = ref 0.0;;
+
+let xxx_type_of_aux' m c t =
+ let t1 = Sys.time () in
+ let res = TypeInference.type_of_aux' m c t in
+ let t2 = Sys.time () in
+ type_of_aux'_add_time := !type_of_aux'_add_time +. t2 -. t1 ;
+ res
+;;
+
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
@@ -36,8 +56,8 @@ let gen_id seed =
 let fresh_id seed ids_to_terms ids_to_father_ids =
  fun father t ->
   let res = gen_id seed in
-   Hashtbl.add ids_to_father_ids res father ;
-   Hashtbl.add ids_to_terms res t ;
+   xxx_add ids_to_father_ids res father ;
+   xxx_add ids_to_terms res t ;
    res
 ;;
 
@@ -60,14 +80,15 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
      ids_to_inner_types metasenv context idrefs t expectedty
 =
  let module D = DoubleTypeInference in
- let module T = CicTypeChecker in
  let module C = Cic in
   let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
-prerr_endline "*************** INIZIO DOUBLE TYPE INFERENCE ************";
+   let time1 = Sys.time () in
    let terms_to_types =
     D.double_type_of metasenv context t expectedty
    in
-prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
+   let time2 = Sys.time () in
+   prerr_endline
+    ("++++++++++++ Tempi della double_type_of: "^ string_of_float (time2 -. time1)) ;
     let rec aux computeinnertypes father context idrefs tt =
      let fresh_id'' = fresh_id' father tt in
      (*CSC: computeinnertypes era true, il che e' proprio sbagliato, no? *)
@@ -90,6 +111,10 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
 (*CSC: type-inference, but the result is very poor. As a very weak    *)
 (*CSC: patch, I apply whd to the computed type. Full beta             *)
 (*CSC: reduction would be a much better option.                       *)
+(*CSC: solo per testare i tempi *)
+(*XXXXXXX *)
+        try
+(* *)
         let {D.synthesized = synthesized; D.expected = expected} =
          if computeinnertypes then
           D.CicHash.find terms_to_types tt
@@ -97,10 +122,13 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
           (* We are already in an inner-type and Coscoy's double *)
           (* type inference algorithm has not been applied.      *)
           {D.synthesized =
-            CicReduction.whd context (T.type_of_aux' metasenv context tt) ;
+(***CSC: patch per provare i tempi
+            CicReduction.whd context (xxx_type_of_aux' metasenv context tt) ; *)
+Cic.Sort Cic.Type ;
            D.expected = None}
         in
-         let innersort = T.type_of_aux' metasenv context synthesized in
+         incr number_new_type_of_aux' ;
+         let innersort = (*XXXXX *) xxx_type_of_aux' metasenv context synthesized (* Cic.Sort Cic.Prop *) in
           let ainnertypes,expected_available =
            if computeinnertypes then
             let annexpected,expected_available =
@@ -120,11 +148,17 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
             None,false
           in
            ainnertypes,synthesized, string_of_sort innersort, expected_available
+(*XXXXXXXX *)
+        with
+         Not_found ->  (* l'inner-type non e' nella tabella ==> sort <> Prop *)
+          (* CSC: Type or Set? I can not tell *)
+          None,Cic.Sort Cic.Type,"Type",false
+(* *)
        in
         let add_inner_type id =
          match ainnertypes with
             None -> ()
-          | Some ainnertypes -> Hashtbl.add ids_to_inner_types id ainnertypes
+          | Some ainnertypes -> xxx_add ids_to_inner_types id ainnertypes
         in
          match tt with
             C.Rel n ->
@@ -133,12 +167,12 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
                  (Some (C.Name s,_)) -> s
                | _ -> raise NameExpected
              in
-              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = "Prop"  && expected_available then
                add_inner_type fresh_id'' ;
               C.ARel (fresh_id'', List.nth idrefs (n-1), n, id)
           | C.Var (uri,exp_named_subst) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
@@ -150,7 +184,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
              let (_,canonical_context,_) =
               List.find (function (m,_,_) -> n = m) metasenv
              in
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              C.AMeta (fresh_id'', n,
@@ -164,21 +198,21 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
           | C.Sort s -> C.ASort (fresh_id'', s)
           | C.Implicit -> C.AImplicit (fresh_id'')
           | C.Cast (v,t) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.ACast (fresh_id'', aux' context idrefs v, aux' context idrefs t)
           | C.Prod (n,s,t) ->
-              Hashtbl.add ids_to_inner_sorts fresh_id''
+              xxx_add ids_to_inner_sorts fresh_id''
                (string_of_sort innertype) ;
-	            let sourcetype = T.type_of_aux' metasenv context s in
-	             Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+	            let sourcetype = xxx_type_of_aux' metasenv context s in
+	             xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
 	              (string_of_sort sourcetype) ;
               let n' =
                match n with
                   C.Anonymous -> n
                 | C.Name n' ->
-                   if D.does_not_occur 1 t then
+                   if TypeInference.does_not_occur 1 t then
                     C.Anonymous
                    else
                     C.Name n'
@@ -187,9 +221,9 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
                 (fresh_id'', n', aux' context idrefs s,
                  aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
           | C.Lambda (n,s,t) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
-	           let sourcetype = T.type_of_aux' metasenv context s in
-	            Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
+	           let sourcetype = xxx_type_of_aux' metasenv context s in
+	            xxx_add ids_to_inner_sorts (source_id_of_id fresh_id'')
 	             (string_of_sort sourcetype) ;
               if innersort = "Prop" then
                begin
@@ -208,19 +242,19 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
                (fresh_id'',n, aux' context idrefs s,
                 aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.ALetIn
               (fresh_id'', n, aux' context idrefs s,
-               aux' ((Some (n, C.Def s))::context) (fresh_id''::idrefs) t)
+               aux' ((Some (n, C.Def(s,None)))::context) (fresh_id''::idrefs) t)
           | C.Appl l ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.AAppl (fresh_id'', List.map (aux' context idrefs) l)
           | C.Const (uri,exp_named_subst) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
@@ -235,7 +269,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
              in
               C.AMutInd (fresh_id'', uri, tyno, exp_named_subst')
           | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop"  && expected_available then
               add_inner_type fresh_id'' ;
              let exp_named_subst' =
@@ -244,7 +278,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
              in
               C.AMutConstruct (fresh_id'', uri, tyno, consno, exp_named_subst')
           | C.MutCase (uri, tyno, outty, term, patterns) ->
-             Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+             xxx_add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
               add_inner_type fresh_id'' ;
              C.AMutCase (fresh_id'', uri, tyno, aux' context idrefs outty,
@@ -256,7 +290,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
              let tys =
               List.map (fun (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) funs
              in
-              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = "Prop" then
                add_inner_type fresh_id'' ;
               C.AFix (fresh_id'', funno,
@@ -273,7 +307,7 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
              let tys =
               List.map (fun (name,ty,_) -> Some (C.Name name, C.Decl ty)) funs
              in
-              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+              xxx_add ids_to_inner_sorts fresh_id'' innersort ;
               if innersort = "Prop" then
                add_inner_type fresh_id'' ;
               C.ACoFix (fresh_id'', funno,
@@ -284,7 +318,12 @@ prerr_endline "*************** FINE DOUBLE TYPE INFERENCE ************";
                 ) fresh_idrefs funs
               )
         in
-         aux true None context idrefs t
+         let timea = Sys.time () in
+         let res = aux true None context idrefs t in
+         let timeb = Sys.time () in
+          prerr_endline
+           ("+++++++++++++ Tempi della aux dentro alla acic_of_cic: "^ string_of_float (timeb -. timea)) ;
+          res
 ;;
 
 let acic_of_cic_context metasenv context idrefs t =
@@ -341,7 +380,6 @@ let acic_object_of_cic_object obj =
         C.AVariable
          ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
-prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ;
        let conjectures' =
         List.map
          (function (i,canonical_context,term) ->
@@ -350,19 +388,20 @@ prerr_endline "************* INIZIO ETA_FIXING (congetture) ********" ;
              (function
                  None -> None
                | Some (n, C.Decl t)-> Some (n, C.Decl (E.eta_fix conjectures t))
-               | Some (n, C.Def t) -> Some (n, C.Def (E.eta_fix conjectures t))
+               | Some (n, C.Def (t,None)) ->
+                  Some (n, C.Def ((E.eta_fix conjectures t),None))
+               | Some (_,C.Def (_,Some _)) -> assert false
              ) canonical_context
            in
            let term' = E.eta_fix conjectures term in
             (i,canonical_context',term')
          ) conjectures
        in
-prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
        let aconjectures =
         List.map
          (function (i,canonical_context,term) as conjecture ->
            let cid = "c" ^ string_of_int !conjectures_seed in
-            Hashtbl.add ids_to_conjectures cid conjecture ;
+            xxx_add ids_to_conjectures cid conjecture ;
             incr conjectures_seed ;
             let idrefs',revacanonical_context =
              let rec aux context idrefs =
@@ -371,7 +410,7 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
                | hyp::tl ->
                   let hid = "h" ^ string_of_int !hypotheses_seed in
                   let new_idrefs = hid::idrefs in
-                   Hashtbl.add ids_to_hypotheses hid hyp ;
+                   xxx_add ids_to_hypotheses hid hyp ;
                    incr hypotheses_seed ;
                    match hyp with
                       (Some (n,C.Decl t)) ->
@@ -382,7 +421,7 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
                           conjectures context idrefs t None
                         in
                          final_idrefs,(hid,Some (n,C.ADecl at))::atl
-                    | (Some (n,C.Def t)) ->
+                    | (Some (n,C.Def (t,_))) ->
                         let final_idrefs,atl =
                          aux (hyp::context) new_idrefs tl in
                         let at =
@@ -404,13 +443,28 @@ prerr_endline "************* INIZIO CIC ==> ACIC (congetture) ********" ;
              in
               (cid,i,(List.rev revacanonical_context),aterm)
          ) conjectures' in
-prerr_endline "*********** INIZIO ETA FIXING PROVA **********";
+       let time1 = Sys.time () in
        let bo' = E.eta_fix conjectures' bo in
        let ty' = E.eta_fix conjectures' ty in
-prerr_endline "*********** INIZIO CIC ==> ACIC PROVA **********";
+       let time2 = Sys.time () in
+       prerr_endline
+        ("++++++++++ Tempi della eta_fix: "^ string_of_float (time2 -. time1)) ;
+       hashtbl_add_time := 0.0 ;
+       type_of_aux'_add_time := 0.0 ;
        let abo =
         acic_term_of_cic_term_context' conjectures' [] [] bo' (Some ty') in
        let aty = acic_term_of_cic_term_context' conjectures' [] [] ty' None in
+       let time3 = Sys.time () in
+       prerr_endline
+        ("++++++++++++ Tempi della hashtbl_add_time: " ^ string_of_float !hashtbl_add_time) ;
+       prerr_endline
+        ("++++++++++++ Tempi della type_of_aux'_add_time(" ^ string_of_int !number_new_type_of_aux' ^ "): " ^ string_of_float !type_of_aux'_add_time) ;
+       prerr_endline
+        ("++++++++++++ Tempi della type_of_aux'_add_time nella double_type_inference(" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_double_work ^ ";" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux'_prop ^ "/" ^ string_of_int !DoubleTypeInference.number_new_type_of_aux' ^ "): " ^ string_of_float !DoubleTypeInference.type_of_aux'_add_time) ;
+       prerr_endline
+        ("++++++++++ Tempi della acic_of_cic: " ^ string_of_float (time3 -. time2)) ;
+       prerr_endline
+        ("++++++++++ Numero di iterazioni della acic_of_cic: " ^ string_of_int !seed) ;
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
     | C.InductiveDefinition (tys,params,paramsno) ->
diff --git a/helm/ocaml/cic_omdoc/eta_fixing.ml b/helm/ocaml/cic_omdoc/eta_fixing.ml
index 876c5c678..81668203d 100644
--- a/helm/ocaml/cic_omdoc/eta_fixing.ml
+++ b/helm/ocaml/cic_omdoc/eta_fixing.ml
@@ -27,6 +27,8 @@ exception ReferenceToVariable;;
 exception RferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 
+let prerr_endline _ = ();;
+
 (* 
 let rec fix_lambdas_wrt_type ty te =
  let module C = Cic in
@@ -163,8 +165,8 @@ let fix_according_to_type ty hd tl =
 
 let eta_fix metasenv t =
  let rec eta_fix' context t = 
-  prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
-  flush stderr ; 
+  (* prerr_endline ("entering aux with: term=" ^ CicPp.ppterm t); 
+  flush stderr ; *)
   let module C = Cic in
   let module S = CicSubstitution in
   match t with
@@ -200,7 +202,7 @@ let eta_fix metasenv t =
         (n, eta_fix' context s, eta_fix' ((Some (n,(C.Decl s)))::context) t)
    | C.LetIn (n,s,t) -> 
        C.LetIn 
-        (n, eta_fix' context s, eta_fix' ((Some (n,(C.Def s)))::context) t)
+        (n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
    | C.Appl l as appl -> 
        let l' =  List.map (eta_fix' context) l 
        in 
@@ -214,11 +216,7 @@ let eta_fix metasenv t =
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
              )
            in
-           let result = fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l'' in
-           if not (CicReduction.are_convertible [] appl result) then 
-             (prerr_endline ("prima :" ^(CicPp.ppterm appl)); 
-              prerr_endline ("dopo :" ^(CicPp.ppterm result)));
-           result
+            fix_according_to_type constant_type (C.Const(uri,exp_named_subst)) l''
         | _ -> C.Appl l' )
    | C.Const (uri,exp_named_subst) ->
        let exp_named_subst' =
@@ -263,7 +261,7 @@ let eta_fix metasenv t =
             List.map (fun (_,t) -> t) constructors 
           else 
 	    let term_type = 
-              CicTypeChecker.type_of_aux' metasenv context term in
+              TypeInference.type_of_aux' metasenv context term in
             (match term_type with
                C.Appl (hd::params) -> 
                  List.map (fun (_,t) -> clean_up t params) constructors
@@ -271,12 +269,7 @@ let eta_fix metasenv t =
        let patterns2 = 
          List.map2 fix_lambdas_wrt_type
            constructor_types patterns in 
-       let dopo = 
-         C.MutCase (uri, tyno, outty',term',patterns2) in
-       if not (CicReduction.are_convertible [] prima dopo) then 
-             (prerr_endline ("prima :" ^(CicPp.ppterm prima)); 
-              prerr_endline ("dopo :" ^(CicPp.ppterm dopo)));
-           dopo
+         C.MutCase (uri, tyno, outty',term',patterns2)
    | C.Fix (funno, funs) ->
        let fun_types = 
          List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) funs in
diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml
index d3f7f0f60..11ed4418c 100644
--- a/helm/ocaml/cic_proof_checking/cicPp.ml
+++ b/helm/ocaml/cic_proof_checking/cicPp.ml
@@ -220,20 +220,21 @@ let ppobj obj =
        List.fold_right
         (fun (n, context, t) i -> 
           let conjectures',name_context =
-	   List.fold_right 
-	    (fun context_entry (i,name_context) ->
-	      (match context_entry with
-	          Some (n,C.Decl at) ->
+	         List.fold_right 
+	          (fun context_entry (i,name_context) ->
+	            (match context_entry with
+	                Some (n,C.Decl at) ->
                    (separate i) ^
-                    string_of_name n ^ ":" ^ pp at name_context ^ " ",
-                   (Some n)::name_context
-	        | Some (n,C.Def at) ->
+                     string_of_name n ^ ":" ^ pp at name_context ^ " ",
+                      (Some n)::name_context
+	              | Some (n,C.Def (at,None)) ->
                    (separate i) ^
-                    string_of_name n ^ ":= " ^ pp at name_context ^ " ",
-                   (Some n)::name_context
+                     string_of_name n ^ ":= " ^ pp at name_context ^ " ",
+                      (Some n)::name_context
                 | None ->
-                   (separate i) ^ "_ :? _ ", None::name_context)
-             ) context ("",[])
+                   (separate i) ^ "_ :? _ ", None::name_context
+                | _ -> assert false)
+            ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
             pp t name_context ^ "\n" ^ i
diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 30b688264..61e7aaaef 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -515,7 +515,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
              match List.nth context (n - 1 - k) with
                 None -> assert false
               | Some (_,C.Decl _) -> None
-              | Some (_,C.Def x) -> Some (S.lift (n - k) x)
+              | Some (_,C.Def (x,_)) -> Some (S.lift (n - k) x)
             end
            with
             _ -> None
@@ -805,11 +805,14 @@ let are_convertible =
               ) true l1 l2
         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
         | (C.Appl l1, C.Appl l2) ->
            (try
              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 987f4b6ed..5dce7c68d 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -53,7 +53,7 @@ let whd context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_, C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_, C.Def bo) -> whdaux l (S.lift n bo)
+         | Some (_, C.Def (bo,_)) -> whdaux l (S.lift n bo)
 	  | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) as t ->
@@ -217,11 +217,14 @@ let are_convertible =
               ) true l1 l2
         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Decl s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.LetIn (name1,s1,t1), C.LetIn(_,s2,t2)) ->
-           aux context s1 s2 && aux ((Some (name1, (C.Def s1)))::context) t1 t2
+           aux context s1 s2 &&
+            aux ((Some (name1, (C.Def (s1,None))))::context) t1 t2
         | (C.Appl l1, C.Appl l2) ->
            (try
              List.fold_right2 (fun  x y b -> aux context x y && b) l1 l2 true 
diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 48d8b2ea9..62dc951aa 100644
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -217,13 +217,16 @@ and does_not_occur context n nn te =
        does_not_occur context n nn te && does_not_occur context n nn ty
     | C.Prod (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+         dest
     | C.Lambda (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
+         dest
     | C.LetIn (name,so,dest) ->
        does_not_occur context n nn so &&
-        does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
+        does_not_occur ((Some (name,(C.Def (so,None))))::context)
+         (n + 1) (nn + 1) dest
     | C.Appl l ->
        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
     | C.Var (_,exp_named_subst)
@@ -403,7 +406,8 @@ and strictly_positive context n nn te =
           (fun x i ->
             i &&
              weakly_positive
-              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
+              ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
+              x
           ) cl' true
    | t -> does_not_occur context n nn t
 
@@ -672,7 +676,7 @@ and check_is_really_smaller_arg context n nn kl x safes te =
         (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)))::context)
+       check_is_really_smaller_arg ((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 *)
@@ -689,7 +693,8 @@ and check_is_really_smaller_arg context n nn kl x safes te =
             match CicEnvironment.get_obj uri with
                C.InductiveDefinition (tl,_,paramsno) ->
                 let tys =
-                 List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
+                 List.map
+                  (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
                 in
                  let (_,isinductive,_,cl) = List.nth tl i in
                   let cl' =
@@ -727,7 +732,8 @@ and check_is_really_smaller_arg context n nn kl x safes te =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map (fun (n,_,ty,_) ->
+                   Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -801,7 +807,8 @@ and guarded_by_destructors context n nn kl x safes =
    | C.Rel n ->
       (match List.nth context (n-1) with
           Some (_,C.Decl _) -> true
-        | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
+        | Some (_,C.Def (bo,_)) ->
+           guarded_by_destructors context n nn kl x safes bo
 	| None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
       )
    | C.Meta _
@@ -820,7 +827,7 @@ and guarded_by_destructors context n nn kl x safes =
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.LetIn (name,so,ta) ->
       guarded_by_destructors context n nn kl x safes so &&
-       guarded_by_destructors ((Some (name,(C.Def so)))::context)
+       guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
       let k = List.nth kl (m - n - 1) in
@@ -850,7 +857,8 @@ and guarded_by_destructors context n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map (fun (n,_,ty,_) ->
+                   Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -892,7 +900,8 @@ and guarded_by_destructors context n nn kl x safes =
                C.InductiveDefinition (tl,_,paramsno) ->
                 let (_,isinductive,_,cl) = List.nth tl i in
                  let tys =
-                  List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
+                  List.map
+                   (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
                  in
                   let cl' =
                    List.map
@@ -1058,8 +1067,8 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
                 [] -> true
               | he::tl ->
                  analyse_branch context so he &&
-                  analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
-                   de tl
+                  analyse_instantiated_type
+                   ((Some (name,(C.Decl so)))::context) de tl
             end
          | C.Lambda _
          | C.LetIn _ ->
@@ -1147,7 +1156,7 @@ and guarded_by_constructors context n nn h te args coInductiveTypeURI =
        let n_plus_len = n + len
        and nn_plus_len = nn + len
        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
-       and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
+       and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
         List.fold_right
          (fun (_,_,ty,bo) i ->
            i && does_not_occur context n nn ty &&
@@ -1293,9 +1302,10 @@ and check_metasenv_consistency metasenv context canonical_context l =
         [] -> []
       | (Some (n,C.Decl t))::tl ->
          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
-      | (Some (n,C.Def t))::tl ->
-         (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+      | (Some (n,C.Def (t,None)))::tl ->
+         (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
       | None::tl -> None::(aux (i+1) tl)
+      | (Some (n,C.Def (_,Some _)))::_ -> assert false
     in
      aux 1 canonical_context
    in
@@ -1304,7 +1314,7 @@ and check_metasenv_consistency metasenv context canonical_context l =
        let res =
         match (t,ct) with
            _,None -> true
-         | Some t,Some (_,C.Def ct) ->
+         | Some t,Some (_,C.Def (ct,_)) ->
             R.are_convertible context t ct
          | Some t,Some (_,C.Decl ct) ->
             R.are_convertible context (type_of_aux' metasenv context t) ct
@@ -1325,8 +1335,11 @@ and type_of_aux' metasenv context t =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t
-          | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
-	  | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
+          | Some (_,C.Def (_,Some ty)) -> S.lift n ty
+          | Some (_,C.Def (bo,None)) ->
+             prerr_endline "##### CASO DA INVESTIGARE E CAPIRE" ;
+             type_of_aux context (S.lift n bo)
+	        | None -> raise (TypeCheckerFailure RelToHiddenHypothesis)
         with
          _ -> raise (TypeCheckerFailure (NotWellTyped "Not a close term"))
        )
@@ -1363,7 +1376,7 @@ and type_of_aux' metasenv context t =
           C.Prod (n,s,type2)
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
-      let _ = type_of_aux context s in
+      let ty = type_of_aux context s in
        (* The type of a LetIn is a LetIn. Extremely slow since the computed
           LetIn is later reduced and maybe also re-checked.
        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
@@ -1377,7 +1390,7 @@ and type_of_aux' metasenv context t =
        (* One-step LetIn reduction. Even faster than the previous solution.
           Moreover the inferred type is closer to the expected one. *)
        (CicSubstitution.subst s
-        (type_of_aux ((Some (n,(C.Def s)))::context) t))
+        (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
    | C.Appl (he::tl) when List.length tl > 0 ->
       let hetype = type_of_aux context he
       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
diff --git a/helm/ocaml/cic_transformations/sequentPp.ml b/helm/ocaml/cic_transformations/sequentPp.ml
index bda66841c..e7b3151ea 100644
--- a/helm/ocaml/cic_transformations/sequentPp.ml
+++ b/helm/ocaml/cic_transformations/sequentPp.ml
@@ -38,10 +38,11 @@ module TextualPp =
          match i with
             Some (n,Cic.Decl t) ->
               print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
-          | Some (n,Cic.Def t) ->
+          | Some (n,Cic.Def (t,None)) ->
               print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
           | None ->
               "_ ?= _\n", None::context
+          | Some (_,Cic.Def (_,Some _)) -> assert false
         in
          output^newoutput,context'
       ) ctx ("",[])
@@ -84,7 +85,7 @@ module XmlPp =
             Hashtbl.add ids_to_hypotheses hid binding ;
             incr hypotheses_seed ;
             match binding with
-               (Some (n,(Cic.Def t as b)) as entry)
+               (Some (n,(Cic.Def (t,None) as b)) as entry)
              | (Some (n,(Cic.Decl t as b)) as entry) ->
                 let acic = acic_of_cic_context context idrefs t None in
                  [< s ;
@@ -97,6 +98,7 @@ module XmlPp =
              | None ->
                 (* Invariant: "" is never looked up *)
                 [< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+             | Some (_,Cic.Def (_,Some _)) -> assert false
          ) context ([<>],[],[])
        )
       in
diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index e5e846982..881c72bfd 100644
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -96,7 +96,9 @@ and type_of_aux' metasenv context t =
        (try
          match List.nth context (n - 1) with
             Some (_,C.Decl t) -> S.lift n t,subst,metasenv
-          | Some (_,C.Def bo) ->
+          | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv
+          | Some (_,C.Def (bo,None)) ->
+             prerr_endline "##### DA INVESTIGARE E CAPIRE" ;
              type_of_aux subst metasenv context (S.lift n bo)
 	  | None -> raise RelToHiddenHypothesis
         with
@@ -160,9 +162,9 @@ and type_of_aux' metasenv context t =
           C.Prod (n,s,type2),subst'''',metasenv''''
    | C.LetIn (n,s,t) ->
       (* only to check if s is well-typed *)
-      let _,subst',metasenv' = type_of_aux subst metasenv context s in
+      let ty,subst',metasenv' = type_of_aux subst metasenv context s in
       let inferredty,subst'',metasenv'' =
-       type_of_aux subst' metasenv' ((Some (n,(C.Def s)))::context) t
+       type_of_aux subst' metasenv' ((Some (n,(C.Def (s,Some ty))))::context) t
       in
        (* One-step LetIn reduction. Even faster than the previous solution.
           Moreover the inferred type is closer to the expected one. *)
@@ -224,9 +226,10 @@ and type_of_aux' metasenv context t =
          [] -> []
        | (Some (n,C.Decl t))::tl ->
           (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
-       | (Some (n,C.Def t))::tl ->
-          (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
+       | (Some (n,C.Def (t,None)))::tl ->
+          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
        | None::tl -> None::(aux (i+1) tl)
+       | (Some (_,C.Def (_,Some _)))::_ -> assert false
      in
       aux 1 canonical_context
     in
@@ -234,7 +237,7 @@ and type_of_aux' metasenv context t =
       (fun (subst,metasenv) t ct -> 
         match (t,ct) with
            _,None -> subst,metasenv
-         | Some t,Some (_,C.Def ct) ->
+         | Some t,Some (_,C.Def (ct,_)) ->
             (try
               CicUnification.fo_unif_subst subst context metasenv t ct
              with _ -> raise MetasenvInconsistency)
diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml
index f7c19073b..306074ec9 100644
--- a/helm/ocaml/cic_unification/cicUnification.ml
+++ b/helm/ocaml/cic_unification/cicUnification.ml
@@ -49,14 +49,14 @@ let position n =
 let restrict to_be_restricted =
   let rec erase i n = 
     function
-	[] -> []
-      |	_::tl when List.mem (n,i) to_be_restricted ->
-	  None::(erase (i+1) n tl) 
+        [] -> []
+      |        _::tl when List.mem (n,i) to_be_restricted ->
+          None::(erase (i+1) n tl) 
       | he::tl -> he::(erase (i+1) n tl) in
   let rec aux =
     function 
-	[] -> []
-      |	(n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
+        [] -> []
+      |        (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in
   aux
 ;;
 
@@ -72,13 +72,13 @@ let delift context metasenv l t =
           C.Rel m   (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *)
                     (*CSC: deliftato la regola per il LetIn                 *)
          else
-	  (match List.nth context (m-k-1) with
-	    Some (_,C.Def t) -> deliftaux k (S.lift m t)
-	  | Some (_,C.Decl t) ->
+          (match List.nth context (m-k-1) with
+            Some (_,C.Def (t,_)) -> deliftaux k (S.lift m t)
+          | Some (_,C.Decl t) ->
              (* It may augment to_be_restricted *)
              ignore (deliftaux k (S.lift m t)) ;
              C.Rel ((position (m-k) l) + k)
-	  | None -> raise RelToHiddenHypothesis)
+          | None -> raise RelToHiddenHypothesis)
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst
@@ -177,7 +177,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
                 (* First possibility:  restriction    *)
                 (* Second possibility: unification    *)
                 (* Third possibility:  convertibility *)
-	        R.are_convertible context t1' t2'
+                R.are_convertible context t1' t2'
          ) true ln lm
        in
         if ok then subst,metasenv else raise UnificationFailed
@@ -186,18 +186,18 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
    | (C.Meta (n,l), t)   
    | (t, C.Meta (n,l)) ->
        let subst',metasenv' =
-	try
-	 let oldt = (List.assoc n subst) in
-	 let lifted_oldt = S.lift_meta l oldt in
-	  fo_unif_subst subst context metasenv lifted_oldt t
-	with Not_found ->
-	 let t',metasenv' = delift context metasenv l t in
-	  (n, t')::subst, metasenv'
+        try
+         let oldt = (List.assoc n subst) in
+         let lifted_oldt = S.lift_meta l oldt in
+          fo_unif_subst subst context metasenv lifted_oldt t
+        with Not_found ->
+         let t',metasenv' = delift context metasenv l t in
+          (n, t')::subst, metasenv'
        in
-	let (_,_,meta_type) = 
-	 List.find (function (m,_,_) -> m=n) metasenv' in
-	let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
-	 fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+        let (_,_,meta_type) = 
+         List.find (function (m,_,_) -> m=n) metasenv' in
+        let tyt = CicTypeChecker.type_of_aux' metasenv' context t in
+         fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
    | (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
@@ -259,7 +259,7 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
             in 
              fo_unif_l subst' metasenv' (l1,l2)
        in
-	fo_unif_l subst metasenv (lr1, lr2) 
+        fo_unif_l subst metasenv (lr1, lr2) 
    | (C.Const _, _) 
    | (_, C.Const _)
    | (C.MutInd  _, _) 
@@ -274,9 +274,9 @@ let rec fo_unif_subst subst context metasenv t1 t2 =
        let subst', metasenv' = 
         fo_unif_subst subst context metasenv outt1 outt2 in
        let subst'',metasenv'' = 
-	fo_unif_subst subst' context metasenv' t1 t2 in
+        fo_unif_subst subst' context metasenv' t1 t2 in
        List.fold_left2 
-	(function (subst,metasenv) ->
+        (function (subst,metasenv) ->
           fo_unif_subst subst context metasenv
         ) (subst'',metasenv'') pl1 pl2 
    | (C.Fix _, _)
@@ -322,24 +322,24 @@ in canonical_context. *)
 let restrict canonical_context m k l =
   let rec erase i = 
     function
-	[] -> []
-      |	None::tl -> None::(erase (i+1) tl)
-      |	he::tl -> 
-	  let i' = (List.nth l (i-1)) in
-	  if i' <= k 
-	   then he::(erase (i+1) tl) (* local variable *) 
-	   else 
-	    let acc = 
-	      (try List.nth canonical_context (i'-k-1)
-	       with Failure _ -> None) in
-	    if acc = None 
-	     then None::(erase (i+1) tl)
-	     else he::(erase (i+1) tl) in
+        [] -> []
+      |        None::tl -> None::(erase (i+1) tl)
+      |        he::tl -> 
+          let i' = (List.nth l (i-1)) in
+          if i' <= k 
+           then he::(erase (i+1) tl) (* local variable *) 
+           else 
+            let acc = 
+              (try List.nth canonical_context (i'-k-1)
+               with Failure _ -> None) in
+            if acc = None 
+             then None::(erase (i+1) tl)
+             else he::(erase (i+1) tl) in
   let rec aux =
     function 
-	[] -> []
-      |	(n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
-      |	hd::tl -> hd::(aux tl)
+        [] -> []
+      |        (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl
+      |        hd::tl -> hd::(aux tl)
   in
    aux
 ;;
@@ -378,39 +378,39 @@ CSCSCS
     | C.Sort _ -> metasenv
     | C.Implicit -> metasenv
     | C.Cast (te,ty) -> 
-	let metasenv' = aux metasenv k te in
-	aux metasenv' k ty
+        let metasenv' = aux metasenv k te in
+        aux metasenv' k ty
     | C.Prod (_,s,t) 
     | C.Lambda (_,s,t) 
     | C.LetIn (_,s,t) ->
-	let metasenv' = aux metasenv k s in
-	aux metasenv' (k+1) t
+        let metasenv' = aux metasenv k s in
+        aux metasenv' (k+1) t
     | C.Appl l ->
-	List.fold_left
-	  (function metasenv -> aux metasenv k) metasenv l
+        List.fold_left
+          (function metasenv -> aux metasenv k) metasenv l
     | C.Const _
     | C.MutInd _ 
     | C.MutConstruct _ -> metasenv
     | C.MutCase (_,_,_,outty,t,pl) ->
-	let metasenv' = aux metasenv k outty in
-	let metasenv'' = aux metasenv' k t in
-	List.fold_left
-	  (function metasenv -> aux metasenv k) metasenv'' pl
+        let metasenv' = aux metasenv k outty in
+        let metasenv'' = aux metasenv' k t in
+        List.fold_left
+          (function metasenv -> aux metasenv k) metasenv'' pl
     | C.Fix (i, fl) ->
        let len = List.length fl in
        List.fold_left
          (fun metasenv f ->
-	   let (_,_,ty,bo) = f in
-	   let metasenv' = aux metasenv k ty in
-	   aux metasenv' (k+len) bo
+           let (_,_,ty,bo) = f in
+           let metasenv' = aux metasenv k ty in
+           aux metasenv' (k+len) bo
          ) metasenv fl
     | C.CoFix (i, fl) ->
-	let len = List.length fl in
+        let len = List.length fl in
         List.fold_left
          (fun metasenv f ->
-	   let (_,ty,bo) = f in
-	   let metasenv' = aux metasenv k ty in
-	   aux metasenv' (k+len) bo
+           let (_,ty,bo) = f in
+           let metasenv' = aux metasenv k ty in
+           aux metasenv' (k+len) bo
          ) metasenv fl
   in aux metasenv 0
 ;;
@@ -427,18 +427,18 @@ let unwind metasenv subst unwinded t =
       C.Rel _ as t -> t,metasenv
     | C.Var _  as t -> t,metasenv
     | C.Meta (i,l) -> 
-	(try
+        (try
           S.lift_meta l (List.assoc i !unwinded), metasenv
          with Not_found ->
            if List.mem i !frozen then raise OccurCheck
            else
             let saved_frozen = !frozen in 
-	    frozen := i::!frozen ;
+            frozen := i::!frozen ;
             let res =
              try
-	      let t = List.assoc i subst in
+              let t = List.assoc i subst in
               let t',metasenv' = um_aux metasenv t in
-	      let _,metasenv'' =
+              let _,metasenv'' =
                let (_,canonical_context,_) = 
                 List.find (function (m,_,_) -> m=i) metasenv
                in
@@ -451,13 +451,13 @@ let unwind metasenv subst unwinded t =
                (* not constrained variable, i.e. free in subst*)
                let l',metasenv' =
                 List.fold_right
-	         (fun t (tl,metasenv) ->
+                 (fun t (tl,metasenv) ->
                    match t with
                       None -> None::tl,metasenv
                     | Some t -> 
-	               let t',metasenv' = um_aux metasenv t in
-	                (Some t')::tl, metasenv'
-	         ) l ([],metasenv)
+                       let t',metasenv' = um_aux metasenv t in
+                        (Some t')::tl, metasenv'
+                 ) l ([],metasenv)
                in
                 C.Meta (i,l'), metasenv'
             in
@@ -485,10 +485,10 @@ let unwind metasenv subst unwinded t =
     | C.Appl (he::tl) ->
        let tl',metasenv' =
         List.fold_right
-	 (fun t (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    t'::tl, metasenv'
-	 ) tl ([],metasenv)
+         (fun t (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            t'::tl, metasenv'
+         ) tl ([],metasenv)
        in
         begin
          match um_aux metasenv' he with
@@ -499,28 +499,28 @@ let unwind metasenv subst unwinded t =
     | C.Const (uri,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.Const (uri,exp_named_subst'),metasenv'
     | C.MutInd (uri,typeno,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.MutInd (uri,typeno,exp_named_subst'),metasenv'
     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
        let exp_named_subst', metasenv' =
         List.fold_right
-	 (fun (uri,t) (tl,metasenv) ->
-	   let t',metasenv' = um_aux metasenv t in
-	    (uri,t')::tl, metasenv'
-	 ) exp_named_subst ([],metasenv)
+         (fun (uri,t) (tl,metasenv) ->
+           let t',metasenv' = um_aux metasenv t in
+            (uri,t')::tl, metasenv'
+         ) exp_named_subst ([],metasenv)
        in
         C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv'
     | C.MutCase (sp,i,outty,t,pl) ->
@@ -528,10 +528,10 @@ let unwind metasenv subst unwinded t =
        let t',metasenv'' = um_aux metasenv' t in
        let pl',metasenv''' =
         List.fold_right
-	 (fun p (pl,metasenv) ->
-	   let p',metasenv' = um_aux metasenv p in
-	    p'::pl, metasenv'
-	 ) pl ([],metasenv'')
+         (fun p (pl,metasenv) ->
+           let p',metasenv' = um_aux metasenv p in
+            p'::pl, metasenv'
+         ) pl ([],metasenv'')
        in
         C.MutCase (sp, i, outty', t', pl'),metasenv'''
     | C.Fix (i, fl) ->
@@ -539,10 +539,10 @@ let unwind metasenv subst unwinded t =
        let liftedfl,metasenv' =
         List.fold_right
          (fun (name, i, ty, bo) (fl,metasenv) ->
-	   let ty',metasenv' = um_aux metasenv ty in
-	   let bo',metasenv'' = um_aux metasenv' bo in
-	    (name, i, ty', bo')::fl,metasenv''
-	 ) fl ([],metasenv)
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, i, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
        in
         C.Fix (i, liftedfl),metasenv'
     | C.CoFix (i, fl) ->
@@ -550,10 +550,10 @@ let unwind metasenv subst unwinded t =
        let liftedfl,metasenv' =
         List.fold_right
          (fun (name, ty, bo) (fl,metasenv) ->
-	   let ty',metasenv' = um_aux metasenv ty in
-	   let bo',metasenv'' = um_aux metasenv' bo in
-	    (name, ty', bo')::fl,metasenv''
-	 ) fl ([],metasenv)
+           let ty',metasenv' = um_aux metasenv ty in
+           let bo',metasenv'' = um_aux metasenv' bo in
+            (name, ty', bo')::fl,metasenv''
+         ) fl ([],metasenv)
        in
         C.CoFix (i, liftedfl),metasenv'
  in
diff --git a/helm/ocaml/tactics/fourierR.ml b/helm/ocaml/tactics/fourierR.ml
index b1aa1a256..a807554c5 100644
--- a/helm/ocaml/tactics/fourierR.ml
+++ b/helm/ocaml/tactics/fourierR.ml
@@ -886,8 +886,10 @@ let rec superlift c n=
   [] -> []
   | Some(name,Cic.Decl(a))::next  -> [Some(name,Cic.Decl(
                   CicSubstitution.lift n a))] @ superlift next (n+1)
-  | Some(name,Cic.Def(a))::next   -> [Some(name,Cic.Def(
-                  CicSubstitution.lift n a))] @ superlift next (n+1)
+  | Some(name,Cic.Def(a,None))::next   -> [Some(name,Cic.Def((
+                  CicSubstitution.lift n a),None))] @ superlift next (n+1)
+  | Some(name,Cic.Def(a,Some ty))::next   -> [Some(name,Cic.Def((
+                  CicSubstitution.lift n a),Some (CicSubstitution.lift n ty)))] @ superlift next (n+1)
   | _::next -> superlift next (n+1) (*??  ??*)
  
 ;;
diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 91cd6198e..8dfdd66c4 100644
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -50,7 +50,7 @@ let lambda_abstract context newmeta ty mk_fresh_name =
          (context',ty,C.Lambda(n',s,bo))
     | C.LetIn (n,s,t) ->
        let (context',ty,bo) =
-        collect_context ((Some (n,(C.Def s)))::context) t
+        collect_context ((Some (n,(C.Def (s,None))))::context) t
        in
         (context',ty,C.LetIn(n,s,bo))
     | _ as t ->
@@ -132,9 +132,10 @@ let classify_metas newmeta in_subst_domain subst_in metasenv =
            match entry with
               Some (n,Cic.Decl s) ->
                Some (n,Cic.Decl (subst_in canonical_context' s))
-            | Some (n,Cic.Def s) ->
-               Some (n,Cic.Def (subst_in canonical_context' s))
+            | Some (n,Cic.Def (s,None)) ->
+               Some (n,Cic.Def ((subst_in canonical_context' s),None))
             | None -> None
+            | Some (_,Cic.Def (_,Some _)) -> assert false
           in
            entry'::canonical_context'
         ) canonical_context []
@@ -361,7 +362,7 @@ let letin_tac
     let fresh_name =
      mk_fresh_name_callback context (Cic.Name "Hletin") ~typ:term in
     let context_for_newmeta =
-     (Some (fresh_name,C.Def term))::context in
+     (Some (fresh_name,C.Def (term,None)))::context in
     let irl =
      identity_relocation_list_for_metavariable context_for_newmeta in
      let newmetaty = CicSubstitution.lift 1 ty in
@@ -547,9 +548,10 @@ let change_tac ~what ~with_what ~status:(proof, goal) =
     let context' =
      List.map
       (function
-          Some (name,Cic.Def  t) -> Some (name,Cic.Def  (replace t))
+          Some (name,Cic.Def (t,None)) -> Some (name,Cic.Def ((replace t),None))
         | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
         | None -> None
+        | Some (_,Cic.Def (_,Some _)) -> assert false
       ) context
     in
      let metasenv' = 
diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 16be77edb..ac5850ca2 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -100,8 +100,9 @@ let subst_meta_in_proof proof meta term newmetasenv =
          List.map
           (function
               Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
-            | Some (n,Cic.Def s) -> Some (n,Cic.Def (subst_in s))
+            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
             | None -> None
+            | Some (_,Cic.Def (_,Some _)) -> assert false
           ) canonical_context
         in
          i,canonical_context',(subst_in ty)
@@ -136,7 +137,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
              (function
                  None -> None
                | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
-               | Some (i,Cic.Def t)  -> Some (i,Cic.Def (subst_in t))
+               | Some (i,Cic.Def (t,None))  ->
+                  Some (i,Cic.Def ((subst_in t),None))
+               | Some (_,Cic.Def (_,Some _))  -> assert false
              ) canonical_context
            in
             (m,canonical_context',subst_in ty)::i
diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index c70be1fb7..9e5aa04ff 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -382,7 +382,7 @@ let reduce context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) -> reduceaux context l (S.lift n bo)
+         | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )
     | C.Var (uri,exp_named_subst) ->
@@ -604,7 +604,7 @@ let simpl context =
       C.Rel n as t ->
        (match List.nth context (n-1) with
            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def bo) ->
+         | Some (_,C.Def (bo,_)) ->
             try_delta_expansion l t (S.lift n bo)
 	 | None -> raise RelToHiddenHypothesis
        )
diff --git a/helm/ocaml/tactics/proofEngineStructuralRules.ml b/helm/ocaml/tactics/proofEngineStructuralRules.ml
index d89420f58..07ddf3a9e 100644
--- a/helm/ocaml/tactics/proofEngineStructuralRules.ml
+++ b/helm/ocaml/tactics/proofEngineStructuralRules.ml
@@ -29,8 +29,9 @@ let clearbody ~hyp ~status:(proof, goal) =
  let module C = Cic in
   match hyp with
      None -> assert false
+   | Some (_, C.Def (_, Some _)) -> assert false
    | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
-   | Some (n_to_clear_body, C.Def term) as hyp_to_clear_body ->
+   | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
       let curi,metasenv,pbo,pty = proof in
        let metano,_,_ = List.find (function (m,_,_) -> m=goal) metasenv in
         let string_of_name =
@@ -56,7 +57,7 @@ let clearbody ~hyp ~status:(proof, goal) =
                          cleared_entry::context
                      | None -> None::context
                      | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
+                     | Some (n,C.Def (t,None)) ->
                         let _ =
                          try
                           CicTypeChecker.type_of_aux' metasenv context t
@@ -71,6 +72,7 @@ let clearbody ~hyp ~status:(proof, goal) =
                              )
                         in
                          entry::context
+                     | Some (_,Cic.Def (_,Some _)) -> assert false
                   ) canonical_context []
                 in
                  let _ =
@@ -113,8 +115,9 @@ let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
                     match entry with
                        t when t == hyp_to_clear -> None::context
                      | None -> None::context
+                     | Some (_,Cic.Def (_,Some _)) -> assert false
                      | Some (n,C.Decl t)
-                     | Some (n,C.Def t) ->
+                     | Some (n,C.Def (t,None)) ->
                         let _ =
                          try
                           CicTypeChecker.type_of_aux' metasenv context t
diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index b29873a1f..55eacc234 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -69,11 +69,12 @@ let reduction_tac ~also_in_hypotheses ~reduction ~terms ~status:(proof,goal) =
       List.fold_right
        (fun entry context ->
          match entry with
-            Some (name,Cic.Def  t) ->
-             (Some (name,Cic.Def  (replace context t)))::context
+            Some (name,Cic.Def (t,None)) ->
+             (Some (name,Cic.Def ((replace context t),None)))::context
           | Some (name,Cic.Decl t) ->
              (Some (name,Cic.Decl (replace context t)))::context
           | None -> None::context
+          | Some (_,Cic.Def (_,Some _)) -> assert false
        ) context []
      else
       context
@@ -110,8 +111,9 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) =
        List.map
         (function
             Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
-          | Some (n,Cic.Def t)  -> Some (n,Cic.Def  (replace t))
+          | Some (n,Cic.Def (t,None))  -> Some (n,Cic.Def ((replace t),None))
           | None -> None
+          | Some (_,Cic.Def (_,Some _)) -> assert false
         ) context
       else
        context
diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 390d97fb7..395768db9 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -39,7 +39,9 @@ let assumption_tac ~status:((proof,goal) as status) =
          (match hd with
              (Some (_, C.Decl t)) when
                (R.are_convertible context (S.lift n t) ty) -> n
-           | (Some (_, C.Def t)) when
+           | (Some (_, C.Def (_,Some ty'))) when
+               (R.are_convertible context ty' ty) -> n
+           | (Some (_, C.Def (t,None))) when
                (R.are_convertible context
                 (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n 
            | _ -> find (n+1) tl