From e73f439e856f456b47ec6381c0c93594eaac5a82 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 24 Feb 2004 16:18:13 +0000
Subject: [PATCH] - patched for new CIC - stat removed from generated queries

---
 helm/ocaml/mathql_generator/cGMatchConclusion.ml | 2 +-
 helm/ocaml/mathql_generator/cGSearchPattern.ml   | 2 +-
 helm/ocaml/mathql_generator/mQueryGenerator.ml   | 7 +++----
 3 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index bb87b461e..42d52a7ac 100644
--- a/helm/ocaml/mathql_generator/cGMatchConclusion.ml
+++ b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
@@ -70,7 +70,7 @@ let levels_of_term metasenv context term =
         Cic.Rel _                        -> l
       | Cic.Meta _                       -> l
       | Cic.Sort _                       -> l 
-      | Cic.Implicit                     -> l 
+      | Cic.Implicit _                   -> l 
       | Cic.Var (u,exp_named_subst)      ->
          let l' = inspect_uri main l u [] v term in
           inspect_exp_named_subst l' (succ v) exp_named_subst
diff --git a/helm/ocaml/mathql_generator/cGSearchPattern.ml b/helm/ocaml/mathql_generator/cGSearchPattern.ml
index 65c955cca..c5167fe85 100644
--- a/helm/ocaml/mathql_generator/cGSearchPattern.ml
+++ b/helm/ocaml/mathql_generator/cGSearchPattern.ml
@@ -101,7 +101,7 @@ let get_constraints term =
             [],[],[!!kind,s']
          | _ -> [],[],[])
     | C.Meta _
-    | C.Implicit -> assert false
+    | C.Implicit _ -> assert false
     | C.Cast (te,_) ->
        (* type ignored *)
        process_type_aux kind te
diff --git a/helm/ocaml/mathql_generator/mQueryGenerator.ml b/helm/ocaml/mathql_generator/mQueryGenerator.ml
index fd349c8ea..7b7204563 100644
--- a/helm/ocaml/mathql_generator/mQueryGenerator.ml
+++ b/helm/ocaml/mathql_generator/mQueryGenerator.ml
@@ -32,7 +32,6 @@ module U = MQGUtil
 
 (* helpers  *****************************************************************)
 
-let stat x       = M.Fun (["stat"], [], [x])
 let diff x y     = M.Fun (["diff"], [], [x; y])
 let union xl     = M.Fun (["union"], [], xl)
 let const s      = M.Const [(s, [])]
@@ -46,7 +45,7 @@ let locate s =
    let query = 
       M.Property (true, M.RefineExact, ["objectName"], [], [], [], [],
                  false, (const s)) 
-   in stat query
+   in query
 
 let unreferred target_pattern source_pattern =
    let query = 
@@ -58,7 +57,7 @@ let unreferred target_pattern source_pattern =
          M.Property (false, M.RefineExact, ["refObj"], ["h:occurrence"],
 	            [], [], [], true, (const source_pattern))
       )
-   in stat query
+   in query
 
 let compose cl = 
    let letin = ref [] in
@@ -152,7 +151,7 @@ let compose cl =
         let f (vvar, msval) x = M.Let (Some vvar, msval, x) in 
         iter f (fun x y z -> x (y z)) ! letin
    in 
-   stat (letin_query (select_query must_query))
+   letin_query (select_query must_query)
 
 (* high-level functions  ****************************************************)
 
-- 
2.39.2