- patched for new CIC

- stat removed from generated queries

diff --git a/helm/ocaml/mathql_generator/cGMatchConclusion.ml b/helm/ocaml/mathql_generator/cGMatchConclusion.ml
index bb87b461efcf548cb7fe1749043c47d0ca5abc4b..42d52a7ac9c6e873fccc950b2b9f28bf6ee93434 100644 (file)
--- 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 65c955cca7652e889aa8a3d622e796c74d159dc3..c5167fe85fe2ec8873470649ef82698da1d88767 100644 (file)
--- 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 fd349c8ea8fdf0f87d3b065f5f7c9ac22bb909f6..7b72045638810878b35ce8c535b936951a949672 100644 (file)
--- 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  ****************************************************)