From 5a4f2e8d76d9744fc6fcb57445d22d922b42fde5 Mon Sep 17 00:00:00 2001
From: natile <??>
Date: Fri, 6 Dec 2002 13:31:17 +0000
Subject: [PATCH] mQueryLevels2.mli added in Makefile.

---
 helm/gTopLevel/.depend              | 1 +
 helm/gTopLevel/Makefile             | 2 +-
 helm/gTopLevel/mQueryGenerator.mli  | 6 ++++++
 helm/gTopLevel/topLevel/topLevel.ml | 9 ++++++++-
 4 files changed, 16 insertions(+), 2 deletions(-)

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index a1f583bb0..5e8706933 100644
--- a/helm/gTopLevel/.depend
+++ b/helm/gTopLevel/.depend
@@ -65,6 +65,7 @@ sequentPp.cmo: cic2Xml.cmi cic2acic.cmi proofEngine.cmi sequentPp.cmi
 sequentPp.cmx: cic2Xml.cmx cic2acic.cmx proofEngine.cmx sequentPp.cmi 
 mQueryLevels.cmo: mQueryLevels.cmi 
 mQueryLevels.cmx: mQueryLevels.cmi 
+mQueryLevels2.cmi: mQueryGenerator.cmi 
 mQueryLevels2.cmo: mQueryLevels2.cmi 
 mQueryLevels2.cmx: mQueryLevels2.cmi 
 mQueryGenerator.cmo: mQueryGenerator.cmi 
diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile
index 9d7c8ac7d..e86d2c179 100644
--- a/helm/gTopLevel/Makefile
+++ b/helm/gTopLevel/Makefile
@@ -24,7 +24,7 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \
           doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
           cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
           logicalOperations.mli sequentPp.ml sequentPp.mli mQueryGenerator.mli \
-          mQueryLevels.ml mQueryLevels2.ml mQueryGenerator.ml gTopLevel.ml
+          mQueryLevels.ml mQueryLevels2.mli mQueryLevels2.ml mQueryGenerator.ml gTopLevel.ml
 
 TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
 	       proofEngineReduction.cmo proofEngineStructuralRules.cmo \
diff --git a/helm/gTopLevel/mQueryGenerator.mli b/helm/gTopLevel/mQueryGenerator.mli
index b1db11142..73cd77b19 100644
--- a/helm/gTopLevel/mQueryGenerator.mli
+++ b/helm/gTopLevel/mQueryGenerator.mli
@@ -44,6 +44,12 @@ type r_obj = (uri * position * depth)
 type r_rel = (position * depth)
 type r_sort = (position * depth * sort) 
 
+(*
+type r_obj = (string * string * int option) 
+type r_rel = (string * int) 
+type r_sort = (string * int * string) 
+*)
+
 type must_restrictions = (r_obj list * r_rel list * r_sort list)
 type only_restrictions =
  (r_obj list option * r_rel list option * r_sort list option)
diff --git a/helm/gTopLevel/topLevel/topLevel.ml b/helm/gTopLevel/topLevel/topLevel.ml
index 745be0767..d021cce85 100644
--- a/helm/gTopLevel/topLevel/topLevel.ml
+++ b/helm/gTopLevel/topLevel/topLevel.ml
@@ -108,10 +108,17 @@ let mbackward n m l =
 	    if Mqint.get_stat () then 
 	       print_string ("? " ^ CicPp.ppterm term ^ nl);
 	    let t0 = Sys.time () in
+	    
+	    
+	    
+	    
+	    
 	    let list_of_must,can = MQueryLevels.out_restr [] [] term in
 	    let len = List.length list_of_must in
 	    let must = if level < len then List.nth list_of_must level else can in
-	    let r = Gen.searchPattern [] [] term must can in
+	   
+	   
+	    let r = Gen.searchPattern must can in
 	    let t1 = Sys.time () -. t0 in
 	    let info = Gen.get_query_info () in
 	    let num = List.nth info 0 in
-- 
2.39.2