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

[helm.git] / helm / gTopLevel / gTopLevel.ml
diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml

index 3774ed0d7b8c5e55fe03677945aa3d343685c245..268d2846ee853b1613a7fa2e08d6d0ab584f5279 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -282,7 +282,9 @@ let call_tactic_with_input tactic rendering_window () =
     in
     let context =
      List.map
-     (function (_,n,_) -> n)
+     (function
+         ProofEngine.Definition (n,_)
+       | ProofEngine.Declaration (n,_) -> n)
       (match !ProofEngine.goal with
           None -> assert false
         | Some (_,(ctx,_)) -> ctx
@@ -379,7 +381,9 @@ let call_tactic_with_input_and_goal_input tactic rendering_window () =
                  in
                  let context =
                   List.map
-                  (function (_,n,_) -> n)
+                  (function
+                      ProofEngine.Definition (n,_)
+                    | ProofEngine.Declaration (n,_) -> n)
                    (match !ProofEngine.goal with
                        None -> assert false
                      | Some (_,(ctx,_)) -> ctx
@@ -479,6 +483,9 @@ let cut rendering_window =
  let change rendering_window =
   call_tactic_with_input_and_goal_input ProofEngine.change rendering_window
  ;;
+let letin rendering_window =
+ call_tactic_with_input ProofEngine.letin rendering_window
+;;
  
  
  let whd_in_scratch scratch_window =
@@ -652,8 +659,12 @@ let check rendering_window scratch_window () =
         None -> []
       | Some (_,(ctx,_)) -> ctx
     in
-    ProofEngine.cic_context_of_context context,
-     List.map (function (_,n,_) -> n) context
+    ProofEngine.cic_context_of_named_context context,
+     List.map
+      (function
+          ProofEngine.Declaration (n,_)
+        | ProofEngine.Definition (n,_) -> n
+      ) context
    in
     (* Do something interesting *)
     let lexbuf = Lexing.from_string input in
@@ -952,6 +963,9 @@ class rendering_window output proofw (label : GMisc.label) =
   let changeb =
    GButton.button ~label:"Change"
     ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let letinb =
+  GButton.button ~label:"Let ... In"
+   ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
   let outputhtml =
    GHtml.xmhtml
     ~source:"<html><body bgColor=\"white\"></body></html>"
@@ -993,6 +1007,7 @@ object(self)
    ignore(foldb#connect#clicked (fold self)) ;
    ignore(cutb#connect#clicked (cut self)) ;
    ignore(changeb#connect#clicked (change self)) ;
+  ignore(letinb#connect#clicked (letin self)) ;
    ignore(introsb#connect#clicked (intros self)) ;
    Logger.log_callback :=
     (Logger.log_to_html ~print_and_flush:(output_html outputhtml))