]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/acic_content/acic2content.ml
Patch to add a debugging string to HExtlib.split_nth reverted
[helm.git] / helm / software / components / acic_content / acic2content.ml
index eddee38b1a51ed2c985df789006c574ae21604e0..c8ff783c3eafab71d645e5bc13005682259a62ae 100644 (file)
@@ -78,7 +78,7 @@ let rec occur uri =
     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
     | C.Cast (te,ty) -> (occur uri te)
     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
-    | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
+    | C.LetIn (_,s,ty,t) -> (occur uri s) or (occur uri ty) or (occur uri t)
     | C.Appl l -> 
         List.fold_left 
           (fun b a -> 
@@ -103,7 +103,7 @@ let get_id =
     | C.AProd (id,_,_,_) -> id
     | C.ACast (id,_,_) -> id
     | C.ALambda (id,_,_,_) -> id
-    | C.ALetIn (id,_,_,_) -> id
+    | C.ALetIn (id,_,_,_,_) -> id
     | C.AAppl (id,_) -> id
     | C.AConst (id,_,_) -> id
     | C.AMutInd (id,_,_,_) -> id
@@ -118,7 +118,11 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
   let module C2A = Cic2acic in
   (* atomic terms are never lifted, according to my policy *)
   function
-      C.ARel (id,_,_,_) -> false
+      C.ARel (id,_,_,_) ->
+         (try 
+            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
+            true;
+          with Not_found -> false) 
     | C.AVar (id,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
@@ -141,7 +145,7 @@ let test_for_lifting ~ids_to_inner_types ~ids_to_inner_sorts=
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
           with Not_found -> false)
-    | C.ALetIn (id,_,_,_) -> 
+    | C.ALetIn (id,_,_,_,_) -> 
          (try 
             ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
             true;
@@ -262,7 +266,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
         { K.conclude_id = gen_id conclude_prefix seed; 
           K.conclude_aref = id;
           K.conclude_method = "Exact";
-          K.conclude_args = [K.Term t];
+          K.conclude_args = [K.Term (false, t)];
           K.conclude_conclusion = 
               try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
               with Not_found -> None
@@ -270,7 +274,7 @@ let generate_exact seed t id name ~ids_to_inner_types =
     }
 ;;
 
-let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
+let generate_intros_let_tac seed id n s ty inner_proof name ~ids_to_inner_types =
   let module C2A = Cic2acic in
   let module C = Cic in
   let module K = Content in
@@ -290,8 +294,9 @@ let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_
               (match inner_proof.K.proof_conclude.K.conclude_conclusion with
                  None -> None
               | Some t -> 
-                  if is_intro then Some (C.AProd ("gen"^id,n,s,t))
-                  else Some (C.ALetIn ("gen"^id,n,s,t)))
+                 match ty with
+                    None -> Some (C.AProd ("gen"^id,n,s,t))
+                  | Some ty -> Some (C.ALetIn ("gen"^id,n,s,ty,t)))
         };
     }
 ;;
@@ -322,18 +327,62 @@ let build_decl_item seed id n s ~ids_to_inner_sorts =
       }
 ;;
 
-let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts =
+let infer_dependent ~headless context metasenv = function
+  | [] -> assert false 
+  | [t] -> [false, t]
+  | he::tl as l ->
+     if headless then
+      List.map (function s -> false,s) l
+     else
+     try
+       let hety,_ = 
+         CicTypeChecker.type_of_aux'
+           metasenv context (Deannotate.deannotate_term he)
+           CicUniv.oblivion_ugraph
+       in
+       let fstorder t =
+         match CicReduction.whd context t with
+         | Cic.Prod _ -> false
+         | _ -> true
+       in
+       let rec dummify_last_tgt t = 
+         match CicReduction.whd context t with
+         | Cic.Prod (n,s,tgt) -> Cic.Prod(n,s, dummify_last_tgt tgt)
+         | _ -> Cic.Implicit None
+       in
+       let rec aux ty = function
+         | [] -> []
+         | t::tl -> 
+              match 
+               FreshNamesGenerator.clean_dummy_dependent_types 
+                 (dummify_last_tgt ty) 
+              with
+              | Cic.Prod (n,src,tgt) ->
+                  (n <> Cic.Anonymous && fstorder src, t) :: 
+                  aux (CicSubstitution.subst 
+                        (Deannotate.deannotate_term t) tgt) tl
+              | _ -> List.map (fun s -> false,s) (t::tl)
+       in
+       (false, he) :: aux hety tl
+     with CicTypeChecker.TypeCheckerFailure _ -> assert false
+;;
+
+let rec build_subproofs_and_args ?(headless=false) seed context metasenv l ~ids_to_inner_types ~ids_to_inner_sorts =
   let module C = Cic in
   let module K = Content in
-  let rec aux =
+  let rec aux =
     function
       [] -> [],[]
-    | t::l1 -> 
-       let subproofs,args = aux l1 in
-        if (test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts) then
+    | (dep, t)::l1 -> 
+       let need_lifting =
+        test_for_lifting t ~ids_to_inner_types ~ids_to_inner_sorts in
+       let subproofs,args = aux (n + if need_lifting then 1 else 0) l1 in
+        if need_lifting then
           let new_subproof = 
             acic2content 
-              seed ~name:"H" ~ids_to_inner_types ~ids_to_inner_sorts t in
+              seed context metasenv 
+               ~name:("H" ^ string_of_int n) ~ids_to_inner_types
+               ~ids_to_inner_sorts t in
           let new_arg = 
             K.Premise
               { K.premise_id = gen_id premise_prefix seed;
@@ -357,7 +406,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                         K.premise_binder = Some b;
                         K.premise_n = Some n
                       }
-                 else (K.Term t)
+                 else (K.Term (dep,t))
              | C.AConst(id,uri,[]) ->
                  let sort = 
                    (try
@@ -369,7 +418,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                         K.lemma_name = UriManager.name_of_uri uri;
                         K.lemma_uri = UriManager.string_of_uri uri
                       }
-                 else (K.Term t)
+                 else (K.Term (dep,t))
              | C.AMutConstruct(id,uri,tyno,consno,[]) ->
                  let sort = 
                    (try
@@ -378,7 +427,7 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                  if sort = `Prop then 
                     let inductive_types =
                       (let o,_ = 
-                        CicEnvironment.get_obj CicUniv.empty_ugraph uri
+                        CicEnvironment.get_obj CicUniv.oblivion_ugraph uri
                       in
                         match o with 
                           | Cic.InductiveDefinition (l,_,_,_) -> l 
@@ -395,11 +444,11 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
                           string_of_int (tyno+1) ^ "/" ^ string_of_int consno ^
                           ")"
                       }
-                 else (K.Term t
-             | _ -> (K.Term t)) in
+                 else (K.Term (dep,t)
+             | _ -> (K.Term (dep,t))) in
           subproofs,hd::args
   in 
-  match (aux l) with
+  match (aux 1 (infer_dependent ~headless context metasenv l)) with
     [p],args -> 
       [{p with K.proof_name = None}], 
         List.map 
@@ -411,13 +460,13 @@ let rec build_subproofs_and_args seed l ~ids_to_inner_types ~ids_to_inner_sorts
 
 and
 
-build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
+build_def_item seed context metasenv id n t ty ~ids_to_inner_sorts ~ids_to_inner_types =
  let module K = Content in
   try
    let sort = Hashtbl.find ids_to_inner_sorts id in
    if sort = `Prop then
        (let p = 
-        (acic2content seed ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
+        (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
        in 
         `Proof p;)
    else 
@@ -425,7 +474,8 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
         { K.def_name = name_of n;
           K.def_id = gen_id definition_prefix seed; 
           K.def_aref = id;
-          K.def_term = t
+          K.def_term = t;
+          K.def_type = ty
         }
   with
    Not_found -> assert false
@@ -434,8 +484,8 @@ build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
 Prop. For debugging purposes this is tested again, possibly raising an 
 Not_a_proof exception *)
 
-and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
-  let rec aux ?name t =
+and acic2content seed context metasenv ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
+  let rec aux ?name context t =
   let module C = Cic in
   let module K = Content in
   let module C2A = Cic2acic in
@@ -459,11 +509,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
     | C.ASort (id,s) -> raise Not_a_proof
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (_,_,_,_) -> raise Not_a_proof
-    | C.ACast (id,v,t) -> aux v
+    | C.ACast (id,v,t) -> aux context v
     | C.ALambda (id,n,s,t) -> 
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = `Prop then 
-          let proof = aux t in
+          let proof = 
+            aux ((Some (n,Cic.Decl (Deannotate.deannotate_term s)))::context) t 
+          in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
                match proof.K.proof_conclude.K.conclude_args with
@@ -478,13 +530,17 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
                   proof'.K.proof_context
             }
           in
-          generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
+          generate_intros_let_tac seed id n s None proof'' name ~ids_to_inner_types
         else 
           raise Not_a_proof 
-    | C.ALetIn (id,n,s,t) ->
+    | C.ALetIn (id,n,s,ty,t) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
         if sort = `Prop then
-          let proof = aux t in
+          let proof =
+            aux
+             ((Some (n,
+              Cic.Def (Deannotate.deannotate_term s,Deannotate.deannotate_term ty)))::context) t 
+          in
           let proof' = 
             if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
                match proof.K.proof_conclude.K.conclude_args with
@@ -495,30 +551,30 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
             { proof' with
                K.proof_name = None;
                K.proof_context = 
-                 ((build_def_item seed (get_id s) n s ids_to_inner_sorts 
+                 ((build_def_item seed context metasenv (get_id s) n s ty ids_to_inner_sorts
                    ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
                  ::proof'.K.proof_context;
             }
           in
-          generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
+          generate_intros_let_tac seed id n s (Some ty) proof'' name ~ids_to_inner_types
         else 
           raise Not_a_proof
     | C.AAppl (id,li) ->
         (try coercion 
-           seed li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try rewrite 
-           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try inductive 
-          seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+          seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
          try transitivity 
-           seed name id li ~ids_to_inner_types ~ids_to_inner_sorts
+           seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts
          with NotApplicable ->
           let subproofs, args =
             build_subproofs_and_args 
-              seed li ~ids_to_inner_types ~ids_to_inner_sorts in
+              seed context metasenv li ~ids_to_inner_types ~ids_to_inner_sorts in
 (*            
           let args_to_lift = 
             List.filter (test_for_lifting ~ids_to_inner_types) li in
@@ -556,7 +612,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
         let inductive_types,noparams =
-          (let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+          (let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
             match o with
                 Cic.Constant _ -> assert false
                | Cic.Variable _ -> assert false
@@ -574,12 +630,13 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
         let pp = 
           let build_proof p (name,arity) =
             let rec make_context_and_body c p n =
-              if n = 0 then c,(aux p)
+              if n = 0 then c,(aux context p)
               else 
                 (match p with
                    Cic.ALambda(idl,vname,s1,t1) ->
                      let ce = 
-                       build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
+                       build_decl_item 
+                         seed idl vname s1 ~ids_to_inner_sorts in
                      make_context_and_body (ce::c) t1 (n-1)
                    | _ -> assert false) in
              let context,body = make_context_and_body [] p arity in
@@ -588,8 +645,8 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           List.map2 build_proof patterns name_and_arities in
         let context,term =
           (match 
-             build_subproofs_and_args 
-               seed ~ids_to_inner_types ~ids_to_inner_sorts [te]
+             build_subproofs_and_args ~headless:true
+               seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts [te]
            with
              l,[t] -> l,t
            | _ -> assert false) in
@@ -603,7 +660,7 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
               K.conclude_method = "Case";
               K.conclude_args = 
                 (K.Aux (UriManager.string_of_uri uri))::
-                (K.Aux (string_of_int typeno))::(K.Term ty)::term::pp;
+                (K.Aux (string_of_int typeno))::(K.Term (false,ty))::term::pp;
               K.conclude_conclusion = 
                 try Some 
                   (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
@@ -611,9 +668,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
              }
         }
     | C.AFix (id, no, funs) -> 
+        let context' = 
+          List.fold_left
+            (fun ctx (_,n,_,ty,_) -> 
+              let ty = Deannotate.deannotate_term ty in
+              Some (Cic.Name n,Cic.Decl ty) :: ctx)
+            [] funs @ context
+        in
         let proofs = 
           List.map 
-            (function (_,name,_,_,bo) -> `Proof (aux ~name bo)) funs in
+            (function (_,name,_,_,bo) -> `Proof (aux context' ~name bo)) funs in
         let fun_name = 
           List.nth (List.map (fun (_,name,_,_,_) -> name) funs) no 
         in
@@ -648,9 +712,16 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
               }
         } 
     | C.ACoFix (id,no,funs) -> 
+        let context' = 
+          List.fold_left
+            (fun ctx (_,n,ty,_) -> 
+              let ty = Deannotate.deannotate_term ty in
+              Some (Cic.Name n,Cic.Decl ty) :: ctx)
+            [] funs @ context
+        in
         let proofs = 
           List.map 
-            (function (_,name,_,bo) -> `Proof (aux ~name bo)) funs in
+            (function (_,name,_,bo) -> `Proof (aux context' ~name bo)) funs in
         let jo = 
           { K.joint_id = gen_id joint_prefix seed;
             K.joint_kind = `CoRecursive;
@@ -682,10 +753,12 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
      in 
      let id = get_id t in
      generate_conversion seed false id t1 ~ids_to_inner_types
-in aux ?name t
+in aux ?name context t
 
-and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
-  let aux ?name = acic2content seed  ~ids_to_inner_types ~ids_to_inner_sorts in
+and inductive seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+  let aux context ?name = 
+    acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+  in
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -707,7 +780,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let ind_str = (prefix ^ ".ind") in 
         let ind_uri = UriManager.uri_of_string ind_str in
         let inductive_types,noparams =
-          (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph ind_uri in
+          (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph ind_uri in
             match o with
                | Cic.InductiveDefinition (l,_,n,_) -> (l,n) 
                | _ -> assert false
@@ -732,8 +805,8 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let args_for_cases, other_args = 
           split no_constructors tail_args in
         let subproofs,other_method_args =
-          build_subproofs_and_args seed other_args
-             ~ids_to_inner_types ~ids_to_inner_sorts in
+          build_subproofs_and_args ~headless:true seed context metasenv
+           other_args ~ids_to_inner_types ~ids_to_inner_sorts in
         let method_args=
           let rec build_method_args =
             function
@@ -746,15 +819,25 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                   let hdarg = 
                     if sortarg = `Prop then
                       let (co,bo) = 
-                        let rec bc = 
+                        let rec bc context 
                           function 
                             Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
+                              let context' = 
+                                Some (n,Cic.Decl(Deannotate.deannotate_term s1))
+                                  ::context
+                              in
                               let ce = 
                                 build_decl_item 
                                   seed idl n s1 ~ids_to_inner_sorts in
                               if (occur ind_uri s) then
                                 ( match t1 with
                                    Cic.ALambda(id2,n2,s2,t2) ->
+                                     let context'' = 
+                                       Some
+                                         (n2,Cic.Decl
+                                           (Deannotate.deannotate_term s2))
+                                       ::context'
+                                     in
                                      let inductive_hyp =
                                        `Hypothesis
                                          { K.dec_name = name_of n2;
@@ -764,21 +847,21 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                                            K.dec_aref = id2;
                                            K.dec_type = s2
                                          } in
-                                     let (context,body) = bc (t,t2) in
+                                     let (context,body) = bc context'' (t,t2) in
                                      (ce::inductive_hyp::context,body)
                                  | _ -> assert false)
                               else 
                                 ( 
-                                let (context,body) = bc (t,t1) in
+                                let (context,body) = bc context' (t,t1) in
                                 (ce::context,body))
-                            | _ , t -> ([],aux t) in
-                        bc (ty,arg) in
+                            | _ , t -> ([],aux context t) in
+                        bc context (ty,arg) in
                       K.ArgProof
                        { bo with
                          K.proof_name = Some name;
                          K.proof_context = co; 
                        };
-                    else (K.Term arg) in
+                    else (K.Term (false,arg)) in
                   hdarg::(build_method_args (tlc,tla))
               | _ -> assert false in
           build_method_args (constructors1,args_for_cases) in
@@ -792,7 +875,7 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                 K.conclude_method = method_name;
                 K.conclude_args =
                   K.Aux (string_of_int no_constructors) 
-                  ::K.Term (C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP)))
+                  ::K.Term (false,(C.AAppl(id,((C.AConst(idc,uri,exp_named_subst))::params_and_IP))))
                   ::method_args@other_method_args;
                 K.conclude_conclusion = 
                    try Some 
@@ -802,24 +885,37 @@ and inductive seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
   | _ -> raise NotApplicable
 
-and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts =
+and coercion seed context metasenv id li ~ids_to_inner_types ~ids_to_inner_sorts =
   match li with
     | ((Cic.AConst _) as he)::tl
     | ((Cic.AMutInd _) as he)::tl
     | ((Cic.AMutConstruct _) as he)::tl when 
-       CoercDb.is_a_coercion' (Deannotate.deannotate_term he) &&
-       !hide_coercions ->
-        let rec last =
-         function
-            [] -> assert false
-          | [t] -> t
-          | _::tl -> last tl
+       (match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+       | None -> false | Some (_,_,_,_,cpos) -> cpos < List.length tl)
+       && !hide_coercions ->
+        let cpos,sats =
+          match CoercDb.is_a_coercion (Deannotate.deannotate_term he) with
+          | None -> assert false
+          | Some (_,_,_,sats,cpos) -> cpos, sats
         in
-          acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts (last tl)
+        let x = List.nth tl cpos in
+        let _,rest = 
+          try HExtlib.split_nth (cpos + sats +1) tl with Failure _ -> [],[] 
+        in
+        if rest = [] then
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           x
+        else
+         acic2content 
+          seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts 
+           (Cic.AAppl (id,x::rest))
     | _ -> raise NotApplicable
 
-and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
-  let aux ?name = acic2content seed ~ids_to_inner_types ~ids_to_inner_sorts in
+and rewrite seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+  let aux context ?name = 
+    acic2content seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts
+  in
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -832,7 +928,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
         let subproofs,arg = 
           (match 
              build_subproofs_and_args 
-               seed ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
+               seed context metasenv 
+                 ~ids_to_inner_types ~ids_to_inner_sorts [List.nth args 3]
            with 
              l,[p] -> l,p
            | _,_ -> assert false) in 
@@ -847,8 +944,8 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                     let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
                       with Not_found -> `Type (CicUniv.fresh())) in
                     if asort = `Prop then
-                      K.ArgProof (aux a)
-                    else K.Term a in
+                      K.ArgProof (aux context a)
+                    else K.Term (false,a) in
                 hd::(ma_aux (n-1) tl) in
           (ma_aux 3 args) in 
           { K.proof_name = name;
@@ -858,9 +955,14 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
             K.proof_conclude = 
               { K.conclude_id = gen_id conclude_prefix seed; 
                 K.conclude_aref = id;
-                K.conclude_method = "Rewrite";
+                K.conclude_method =
+                 if UriManager.eq uri HelmLibraryObjects.Logic.eq_ind_URI
+                 || LibraryObjects.is_eq_ind_URI uri then
+                  "RewriteLR"
+                 else
+                  "RewriteRL";
                 K.conclude_args = 
-                  K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
+                  K.Term (false,(C.AConst (sid,uri,exp_named_subst)))::method_args;
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
@@ -870,7 +972,9 @@ and rewrite seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
       else raise NotApplicable
   | _ -> raise NotApplicable
 
-and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
+and transitivity 
+  seed context metasenv name id li ~ids_to_inner_types ~ids_to_inner_sorts 
+=
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -892,13 +996,13 @@ and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
                 K.conclude_aref = id;
                 K.conclude_method = "Eq_chain";
                 K.conclude_args = 
-                   K.Term t1::
+                   K.Term (false,t1)::
                     (transitivity_aux 
-                       seed ~ids_to_inner_types ~ids_to_inner_sorts p1)@
-                    [K.Term t2]@
+                       seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+                     @ [K.Term (false,t2)]@
                     (transitivity_aux 
-                       seed ~ids_to_inner_types ~ids_to_inner_sorts p2)@
-                    [K.Term t3];
+                       seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
+                     @ [K.Term (false,t3)];
                 K.conclude_conclusion = 
                    try Some 
                      (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
@@ -907,7 +1011,7 @@ and transitivity seed name id li ~ids_to_inner_types ~ids_to_inner_sorts =
           } 
     | _ -> raise NotApplicable
 
-and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
+and transitivity_aux seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts t =
   let module C2A = Cic2acic in
   let module K = Content in
   let module C = Cic in
@@ -920,11 +1024,13 @@ and transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts t =
            | [_;t1;t2;t3;p1;p2] -> t1,t2,t3,p1,p2
            | _ -> raise NotApplicable
        in
-          (transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p1)
-         @[K.Term t2]
-         @(transitivity_aux seed ~ids_to_inner_types ~ids_to_inner_sorts p2)
+          (transitivity_aux 
+            seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p1)
+         @[K.Term (false,t2)]
+         @(transitivity_aux 
+            seed context metasenv ~ids_to_inner_types ~ids_to_inner_sorts p2)
     | _ -> [K.ArgProof 
-       (acic2content seed ~ids_to_inner_sorts ~ids_to_inner_types t)]
+       (acic2content seed context metasenv ~ids_to_inner_sorts ~ids_to_inner_types t)]
 
 ;; 
 
@@ -948,7 +1054,7 @@ let map_conjectures
               K.dec_aref = get_id t;
               K.dec_type = t
             })
-     | (id,Some (name,Cic.ADef t)) ->
+     | (id,Some (name,Cic.ADef (t,ty))) ->
          Some
           (* We should call build_def_item, but we have not computed *)
           (* the inner-types ==> we always produce a declaration     *)
@@ -956,7 +1062,8 @@ let map_conjectures
              { K.def_name = name_of name;
                K.def_id = gen_id definition_prefix seed; 
                K.def_aref = get_id t;
-               K.def_term = t
+               K.def_term = t;
+               K.def_type = ty
              })
    ) context
  in
@@ -984,7 +1091,7 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) =
               K.dec_aref = get_id t;
               K.dec_type = t
             })
-     | (id,Some (name,Cic.ADef t)) ->
+     | (id,Some (name,Cic.ADef (t,ty))) ->
          Some
           (* We should call build_def_item, but we have not computed *)
           (* the inner-types ==> we always produce a declaration     *)
@@ -992,7 +1099,8 @@ let map_sequent ((id,n,context,ty):Cic.annconjecture) =
              { K.def_name = name_of name;
                K.def_id = id; 
                K.def_aref = get_id t;
-               K.def_term = t
+               K.def_term = t;
+               K.def_type = ty
              })
    ) context
  in
@@ -1012,12 +1120,14 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
              (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
              conjectures),
           `Def (K.Const,ty,
-            build_def_item seed (get_id bo) (C.Name n) bo 
+           build_def_item 
+             seed [] (Deannotate.deannotate_conjectures conjectures) 
+             (get_id bo) (C.Name n) bo ty
              ~ids_to_inner_sorts ~ids_to_inner_types))
     | C.AConstant (_,_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Const,ty,
-             build_def_item seed (get_id bo) (C.Name n) bo 
+           build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
                ~ids_to_inner_sorts ~ids_to_inner_types))
     | C.AConstant (id,_,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
@@ -1027,7 +1137,7 @@ let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types =
     | C.AVariable (_,n,Some bo,ty,params,_) ->
          (gen_id object_prefix seed, params, None,
            `Def (K.Var,ty,
-             build_def_item seed (get_id bo) (C.Name n) bo
+           build_def_item seed [] [] (get_id bo) (C.Name n) bo ty
                ~ids_to_inner_sorts ~ids_to_inner_types))
     | C.AVariable (id,n,None,ty,params,_) ->
          (gen_id object_prefix seed, params, None,