mQueryLevels2.mli added in Makefile.

diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend
index a1f583bb0ef97a93dd99c2839811d7261ce76e50..5e8706933e83e0cb67eea83b2ab9e63bc83e7e9b 100644 (file)
--- 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 9d7c8ac7da05e0a499b4c6ef7a109ea0a0b0df95..e86d2c1794679ee8ab8f4cdcb9687401736e97b9 100644 (file)
--- 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 b1db11142a9c0920e63d16319d1b18a91d67f1c1..73cd77b195796aae2a62a1e433cec933ccd1e52e 100644 (file)
--- 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 745be0767a6b137a7937447e20b2757a5e929316..d021cce856eb3c69c49b76c0db45b465f760a47a 100644 (file)
--- 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