* The interface of CicTypeChecker now allows the usage of definitions in

[helm.git] / helm / gTopLevel / logicalOperations.ml

diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml
index 277451bf42ed2774e99c46303822c03f47f1dec0..80f7d04cbfde32f72f49ef650d6ad412c93087b6 100644 (file)
--- a/helm/gTopLevel/logicalOperations.ml
+++ b/helm/gTopLevel/logicalOperations.ml
@@ -20,11 +20,11 @@ let get_context ids_to_terms ids_to_father_ids =
          | C.Sort _
          | C.Implicit
          | C.Cast _ -> []
-         | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
+         | C.Prod (n,s,t) when t == term -> [P.Declaration (n,s)]
          | C.Prod _ -> []
-         | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
+         | C.Lambda (n,s,t) when t == term -> [P.Declaration (n,s)]
          | C.Lambda _ -> []
-         | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
+         | C.LetIn (n,s,t) when t == term -> [P.Definition (n,s)]
          | C.LetIn _ -> []
          | C.Appl _
          | C.Const _ -> []
@@ -37,7 +37,7 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,_,ty,bo) ->
-                let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
+                let res = (P.Definition (C.Name name, C.Fix (!counter,ifl))) in
                  incr counter ;
                  res
               ) ifl
@@ -45,7 +45,7 @@ let get_context ids_to_terms ids_to_father_ids =
             let counter = ref 0 in
              List.rev_map
               (function (name,ty,bo) ->
-                let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
+                let res = (P.Definition (C.Name name, C.CoFix (!counter,ifl))) in
                  incr counter ;
                  res
               ) ifl
@@ -63,27 +63,21 @@ let to_sequent id ids_to_terms ids_to_father_ids =
  let module P = ProofEngine in
   let term = Hashtbl.find ids_to_terms id in
   let context = get_context ids_to_terms ids_to_father_ids id in
-   let type_checker_env_of_context =
-    List.map
-     (function
-         P.Declaration,_,t -> t
-       | P.Definition,_,_ -> raise NotImplemented
-     ) context
+   let metasenv =
+    match !P.proof with
+       None -> assert false
+     | Some (_,metasenv,_,_) -> metasenv
    in
-    let metasenv =
-     match !P.proof with
-        None -> assert false
-      | Some (_,metasenv,_,_) -> metasenv
+    let ty =
+     CicTypeChecker.type_of_aux' metasenv
+      (P.cic_context_of_named_context context) term
     in
-     let ty =
-      CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
+     let (meta,perforated) =
+      (* If the selected term is already a meta, we return it. *)
+      (* Otherwise, we are trying to refine a non-meta term... *)
+      match term with
+         Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
+       | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
      in
-      let (meta,perforated) =
-       (* If the selected term is already a meta, we return it. *)
-       (* Otherwise, we are trying to refine a non-meta term... *)
-       match term with
-          Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
-        | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
-      in
-       perforated
+      perforated
 ;;