From: Ferruccio Guidi Date: Thu, 4 Sep 2003 13:07:26 +0000 (+0000) Subject: CGLocateInductive patched X-Git-Tag: v0_0_1~53 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36d9dada5eb3894d96c807781e1056b73a1c0a79;p=helm.git CGLocateInductive patched --- diff --git a/helm/mathql_test/mqgtop.ml b/helm/mathql_test/mqgtop.ml index aba3bb3d4..edf714b1e 100644 --- a/helm/mathql_test/mqgtop.ml +++ b/helm/mathql_test/mqgtop.ml @@ -232,7 +232,7 @@ let mbackward n m l = let inductive l = let queries = ref [] in - let univ = Some C3.universe in + let univ = None in let handle = get_handle () in let rec aux = function | [] -> () diff --git a/helm/ocaml/mathql_generator/.depend b/helm/ocaml/mathql_generator/.depend index ef727f7b9..820add841 100644 --- a/helm/ocaml/mathql_generator/.depend +++ b/helm/ocaml/mathql_generator/.depend @@ -11,5 +11,5 @@ cGMatchConclusion.cmo: mQGTypes.cmo cGMatchConclusion.cmi cGMatchConclusion.cmx: mQGTypes.cmx cGMatchConclusion.cmi cGSearchPattern.cmo: mQGTypes.cmo mQGUtil.cmi cGSearchPattern.cmi cGSearchPattern.cmx: mQGTypes.cmx mQGUtil.cmx cGSearchPattern.cmi -cGLocateInductive.cmo: cGSearchPattern.cmi mQGTypes.cmo cGLocateInductive.cmi -cGLocateInductive.cmx: cGSearchPattern.cmx mQGTypes.cmx cGLocateInductive.cmi +cGLocateInductive.cmo: mQGTypes.cmo cGLocateInductive.cmi +cGLocateInductive.cmx: mQGTypes.cmx cGLocateInductive.cmi diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.ml b/helm/ocaml/mathql_generator/cGLocateInductive.ml index 04a2f2ad4..032060fd3 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.ml +++ b/helm/ocaml/mathql_generator/cGLocateInductive.ml @@ -38,5 +38,3 @@ let get_constraints = function let constr_sort = [(`MainHypothesis (Some 1), MQGTypes.Prop)] in (constr_obj, constr_rel, constr_sort) | _ -> raise NotAnInductiveDefinition - -let universe = CGSearchPattern.universe diff --git a/helm/ocaml/mathql_generator/cGLocateInductive.mli b/helm/ocaml/mathql_generator/cGLocateInductive.mli index e4c6c1fa9..b6a51401e 100644 --- a/helm/ocaml/mathql_generator/cGLocateInductive.mli +++ b/helm/ocaml/mathql_generator/cGLocateInductive.mli @@ -28,6 +28,4 @@ val get_constraints : Cic.term -> MQGTypes.must_restrictions -val universe : MQGTypes.universe - exception NotAnInductiveDefinition diff --git a/helm/searchEngine/searchEngine.ml b/helm/searchEngine/searchEngine.ml index 622f10bd5..f7fae9481 100644 --- a/helm/searchEngine/searchEngine.ml +++ b/helm/searchEngine/searchEngine.ml @@ -178,20 +178,20 @@ let contype = "Content-Type", "text/html";; let get_constraints term = function | "/locateInductivePrinciple" -> - CGLocateInductive.universe, + None, (CGLocateInductive.get_constraints term), (None,None,None) | "/searchPattern" -> let constr_obj, constr_rel, constr_sort = CGSearchPattern.get_constraints term in - CGSearchPattern.universe, - (constr_obj, constr_rel, constr_sort), - (Some constr_obj, Some constr_rel, Some constr_sort) + (Some CGSearchPattern.universe), + (constr_obj, constr_rel, constr_sort), + (Some constr_obj, Some constr_rel, Some constr_sort) | "/matchConclusion" -> let list_of_must, only = CGMatchConclusion.get_constraints [] [] term in (* FG: there is no way to choose the block number ***************************) let block = pred (List.length list_of_must) in - CGMatchConclusion.universe, + (Some CGMatchConclusion.universe), (List.nth list_of_must block, [], []), (Some only, None, None) | _ -> assert false ;; @@ -579,7 +579,7 @@ List.iter (fun u -> prerr_endline ("<" ^ Netencoding.Url.decode u ^ ">")) tail; raise Chat_unfinished) in let query = - G.query_of_constraints (Some universe) must'' only' + G.query_of_constraints universe must'' only' in let results = MQueryInterpreter.execute mqi_handle query in Http_daemon.send_basic_headers ~code:200 outchan ;