From 4cb4d286a1fdcb150c2848a9d21ac3486906c317 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 9 Mar 2005 10:22:39 +0000
Subject: [PATCH] support for terms with metas in check

---
 helm/matita/matitaInterpreter.ml |  6 +++---
 helm/matita/matitaMathView.ml    | 10 +++++-----
 helm/matita/matitaTypes.ml       |  2 +-
 helm/matita/matitaTypes.mli      |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/helm/matita/matitaInterpreter.ml b/helm/matita/matitaInterpreter.ml
index 9440e8466..e578a3eb0 100644
--- a/helm/matita/matitaInterpreter.ml
+++ b/helm/matita/matitaInterpreter.ml
@@ -139,10 +139,10 @@ class sharedState
             !(Lazy.force basedir));
           Quiet
       | TacticAst.Command (TacticAst.Check term) ->
-          let (_, _, term,ugraph) = 
+          let (_, metasenv, term,ugraph) = 
 	    MatitaCicMisc.disambiguate ~disambiguator ~currentProof term 
 	  in
-          let (context, metasenv) =
+          let (context, _) =
             MatitaCicMisc.get_context_and_metasenv currentProof
           in
 (* this is the Eval Compute
@@ -155,7 +155,7 @@ class sharedState
 	    (* TASSI: here ugraph1 is unused.... FIXME *)
           let expr = Cic.Cast (term, ty) in
           (match mathViewer with
-          | Some v -> v#checkTerm (`Cic expr)
+          | Some v -> v#checkTerm (`Cic (expr, metasenv))
           | _ -> ());
           Quiet
       | TacticAst.Command (TacticAst.Search_pat (search_kind, pat)) ->
diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7aa54f2c7..59324f1a1 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -431,13 +431,13 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
       self#_loadTermAst (disambiguator#parserr#parseTerm (Stream.of_string s))
 
     method private _loadTermAst ast =
-      let (_, _, term, _) =
+      let (_, metasenv, term, _) =
         MatitaCicMisc.disambiguate ~disambiguator ~currentProof ast
       in
-      self#_loadTermCic term
+      self#_loadTermCic term metasenv
 
-    method private _loadTermCic term =
-      let (context, metasenv) =
+    method private _loadTermCic term metasenv =
+      let (context, _) =
         MatitaCicMisc.get_context_and_metasenv currentProof
       in
       let dummyno = CicMkImplicit.new_meta metasenv [] in
@@ -448,7 +448,7 @@ class cicBrowser ~(history:string MatitaMisc.history) () =
       handle_error (fun () ->
         (match src with
         | `Ast ast -> self#_loadTermAst ast
-        | `Cic cic -> self#_loadTermCic cic
+        | `Cic (cic, metasenv) -> self#_loadTermCic cic metasenv
         | `String s -> self#_loadTerm s);
         self#setUri "check")
 
diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 73a5da1a1..95618d142 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -160,7 +160,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
 
diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index 1db5bb0de..262999672 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -198,7 +198,7 @@ class type interpreter =
 
 type term_source =
   [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term
+  | `Cic of Cic.term * Cic.metasenv
   | `String of string
   ]
 
-- 
2.39.2