From 1e18535e2671bd62d2ad82ab8d5c5201545d0bdb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Jan 2005 09:32:35 +0000 Subject: [PATCH] - removed applyStylesheets - added Print and print_kind to AST - added coercion module --- .../cic_disambiguation/cicTextualParser2.ml | 92 +++++++-- helm/ocaml/cic_disambiguation/disambiguate.ml | 5 +- helm/ocaml/cic_transformations/.depend | 52 +++--- helm/ocaml/cic_transformations/Makefile | 2 +- .../cic_transformations/applyStylesheets.ml | 175 ------------------ .../cic_transformations/applyStylesheets.mli | 51 ----- helm/ocaml/cic_transformations/tacticAst.ml | 3 + helm/ocaml/cic_unification/coercGraph.ml | 4 +- 8 files changed, 112 insertions(+), 272 deletions(-) delete mode 100644 helm/ocaml/cic_transformations/applyStylesheets.ml delete mode 100644 helm/ocaml/cic_transformations/applyStylesheets.mli diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index 478e97d39..452593005 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -75,6 +75,10 @@ let name_of_string = function | "_" -> Cic.Anonymous | s -> Cic.Name s +let string_of_name = function + | Cic.Anonymous -> "_" + | Cic.Name s -> s + let int_opt = function | None -> None | Some lexeme -> Some (int_of_string lexeme) @@ -120,8 +124,8 @@ EXTEND ]; typed_name: [ [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" -> - (name_of_string i, Some typ) - | i = IDENT -> (name_of_string i, None) + (Cic.Name i, Some typ) + | i = IDENT -> (Cic.Name i, None) ] ]; subst: [ @@ -150,25 +154,63 @@ EXTEND (head, vars) ] ]; + let_defs:[ + [ defs = LIST1 [ + var = typed_name; + args = LIST1 [ + PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":"; + ty = term; PAREN ")" -> + (names, ty) + ]; + index_name = OPT [ IDENT "on"; idx = IDENT -> idx ]; + SYMBOL <:unicode> (* ≝ *); + t1 = term -> + let rec list_of_lambda ty final_term = function + | [] -> final_term + | name::tl -> + CicAst.Binder (`Lambda, (Cic.Name name, Some ty), + list_of_lambda ty final_term tl) + in + let rec lambda_of_arg_list final_term = function + | [] -> final_term + | (l,ty)::tl -> + list_of_lambda ty (lambda_of_arg_list final_term tl) l + in + let t1' = lambda_of_arg_list t1 args in + let rec get_position_of name n = function + | [] -> (None,n) + | nam::tl -> + if nam = name then + (Some n,n) + else + (get_position_of name (n+1) tl) + in + let rec find_arg name n = function + | [] -> (fail loc (sprintf "Argument %s not found" name)) + | (l,_)::tl -> + let (got,len) = get_position_of name 0 l in + (match got with + | None -> (find_arg name (n+len) tl) + | Some where -> n + where) + in + let index = + (match index_name with + | None -> 0 + | (Some name) -> find_arg name 0 args) + in + (var, t1', index) + ] SEP "and" -> defs + ]]; constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ]; term0: [ [ t = term; EOI -> return_term loc t ] ]; term: [ "letin" NONA [ "let"; var = typed_name; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) + SYMBOL <:unicode> (* ≝ *); t1 = term; "in"; t2 = term -> return_term loc (CicAst.LetIn (var, t1, t2)) | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; - defs = LIST1 [ - var = typed_name; - index = OPT [ PAREN "("; index = NUM; PAREN ")" -> - int_of_string index - ]; - SYMBOL "="; (* SYMBOL <:unicode> (* ≝ *); *) - t1 = term -> - (var, t1, (match index with None -> 0 | Some i -> i)) - ] SEP "and"; - "in"; body = term -> + defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] | "binder" RIGHTA @@ -235,7 +277,8 @@ EXTEND "with"; PAREN "["; patterns = LIST0 [ - lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term -> + lhs = pattern; SYMBOL <:unicode> (* ⇒ *); rhs = term + -> ((lhs: CicAst.case_pattern), rhs) ] SEP SYMBOL "|"; PAREN "]" -> @@ -406,17 +449,38 @@ EXTEND let ind_types = fst_ind_type :: tl_ind_types in (params, ind_types) ] ]; + print_kind: [ + [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ] + -> `Env + ] ]; + command: [ [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof | [ IDENT "quit" | IDENT "Quit" ] -> return_command loc TacticAst.Quit | [ IDENT "qed" | IDENT "Qed" ] -> return_command loc (TacticAst.Qed None) + | [ IDENT "print" | IDENT "Print" ]; + print_kind = print_kind -> + return_command loc (TacticAst.Print print_kind) | [ IDENT "save" | IDENT "Save" ]; name = IDENT -> return_command loc (TacticAst.Qed (Some name)) | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term; body = OPT [ SYMBOL <:unicode> (* ≝ *); body = term -> body ] -> return_command loc (TacticAst.Theorem (flavour, name, typ, body)) + | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ]; + defs = let_defs -> + let name,ty = + match defs with + | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty + | ((Cic.Name name,None),_,_) :: _ -> + fail loc ("No type given for " ^ name) + | _ -> assert false + in + let body = CicAst.Ident (name,None) in + TacticAst.Theorem(`Definition, Some name, ty, + Some (CicAst.LetRec (ind_kind, defs, body))) + | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec -> let (params, ind_types) = spec in return_command loc (TacticAst.Inductive (params, ind_types)) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 7237c8fb7..0ff738fda 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -35,6 +35,7 @@ exception NoWellTypedInterpretation exception Try_again let debug = false +let debug = true let debug_print = if debug then prerr_endline else ignore (* @@ -79,7 +80,9 @@ let refine metasenv context term ugraph = let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () = try snd (Environment.find item env) env num args - with Not_found -> assert false + with Not_found -> + failwith ("Domain item not found: " ^ + (DisambiguateTypes.string_of_domain_item item)) (* TODO move it to Cic *) let find_in_environment name context = diff --git a/helm/ocaml/cic_transformations/.depend b/helm/ocaml/cic_transformations/.depend index c32d3be16..02bb63b9e 100644 --- a/helm/ocaml/cic_transformations/.depend +++ b/helm/ocaml/cic_transformations/.depend @@ -3,12 +3,12 @@ cicAst.cmx: cicAst.cmi contentTable.cmi: cicAst.cmi acic2Ast.cmi: cicAst.cmi cicAstPp.cmi: cicAst.cmi -ast2pres.cmi: mpresentation.cmi cicAst.cmi box.cmi -content2pres.cmi: mpresentation.cmi box.cmi -sequent2pres.cmi: mpresentation.cmi box.cmi -tacticAstPp.cmi: tacticAst.cmo cicAst.cmi -boxPp.cmi: cicAst.cmi box.cmi -tacticAst2Box.cmi: tacticAst.cmo cicAst.cmi box.cmi +ast2pres.cmi: box.cmi cicAst.cmi mpresentation.cmi +content2pres.cmi: box.cmi mpresentation.cmi +sequent2pres.cmi: box.cmi mpresentation.cmi +tacticAstPp.cmi: cicAst.cmi tacticAst.cmo +boxPp.cmi: box.cmi cicAst.cmi +tacticAst2Box.cmi: box.cmi cicAst.cmi tacticAst.cmo tacticAst.cmo: cicAst.cmi tacticAst.cmx: cicAst.cmx cicAst.cmo: cicAst.cmi @@ -25,15 +25,15 @@ acic2Ast.cmo: cicAst.cmi acic2Ast.cmi acic2Ast.cmx: cicAst.cmx acic2Ast.cmi cicAstPp.cmo: cicAst.cmi cicAstPp.cmi cicAstPp.cmx: cicAst.cmx cicAstPp.cmi -ast2pres.cmo: mpresentation.cmi cicAst.cmi box.cmi ast2pres.cmi -ast2pres.cmx: mpresentation.cmx cicAst.cmx box.cmx ast2pres.cmi -content2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \ +ast2pres.cmo: box.cmi cicAst.cmi mpresentation.cmi ast2pres.cmi +ast2pres.cmx: box.cmx cicAst.cmx mpresentation.cmx ast2pres.cmi +content2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \ content2pres.cmi -content2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \ +content2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \ content2pres.cmi -sequent2pres.cmo: mpresentation.cmi box.cmi ast2pres.cmi acic2Ast.cmi \ +sequent2pres.cmo: acic2Ast.cmi ast2pres.cmi box.cmi mpresentation.cmi \ sequent2pres.cmi -sequent2pres.cmx: mpresentation.cmx box.cmx ast2pres.cmx acic2Ast.cmx \ +sequent2pres.cmx: acic2Ast.cmx ast2pres.cmx box.cmx mpresentation.cmx \ sequent2pres.cmi misc.cmo: misc.cmi misc.cmx: misc.cmi @@ -41,19 +41,15 @@ xml2Gdome.cmo: xml2Gdome.cmi xml2Gdome.cmx: xml2Gdome.cmi sequentPp.cmo: cic2Xml.cmi sequentPp.cmi sequentPp.cmx: cic2Xml.cmx sequentPp.cmi -applyStylesheets.cmo: xml2Gdome.cmi sequentPp.cmi misc.cmi cic2Xml.cmi \ - applyStylesheets.cmi -applyStylesheets.cmx: xml2Gdome.cmx sequentPp.cmx misc.cmx cic2Xml.cmx \ - applyStylesheets.cmi -applyTransformation.cmo: xml2Gdome.cmi sequent2pres.cmi mpresentation.cmi \ - misc.cmi content2pres.cmi box.cmi ast2pres.cmi applyTransformation.cmi -applyTransformation.cmx: xml2Gdome.cmx sequent2pres.cmx mpresentation.cmx \ - misc.cmx content2pres.cmx box.cmx ast2pres.cmx applyTransformation.cmi -tacticAstPp.cmo: tacticAst.cmo cicAstPp.cmi tacticAstPp.cmi -tacticAstPp.cmx: tacticAst.cmx cicAstPp.cmx tacticAstPp.cmi -boxPp.cmo: cicAstPp.cmi box.cmi ast2pres.cmi boxPp.cmi -boxPp.cmx: cicAstPp.cmx box.cmx ast2pres.cmx boxPp.cmi -tacticAst2Box.cmo: tacticAstPp.cmi tacticAst.cmo cicAstPp.cmi boxPp.cmi \ - box.cmi ast2pres.cmi tacticAst2Box.cmi -tacticAst2Box.cmx: tacticAstPp.cmx tacticAst.cmx cicAstPp.cmx boxPp.cmx \ - box.cmx ast2pres.cmx tacticAst2Box.cmi +applyTransformation.cmo: ast2pres.cmi box.cmi content2pres.cmi misc.cmi \ + mpresentation.cmi sequent2pres.cmi xml2Gdome.cmi applyTransformation.cmi +applyTransformation.cmx: ast2pres.cmx box.cmx content2pres.cmx misc.cmx \ + mpresentation.cmx sequent2pres.cmx xml2Gdome.cmx applyTransformation.cmi +tacticAstPp.cmo: cicAstPp.cmi tacticAst.cmo tacticAstPp.cmi +tacticAstPp.cmx: cicAstPp.cmx tacticAst.cmx tacticAstPp.cmi +boxPp.cmo: ast2pres.cmi box.cmi cicAstPp.cmi boxPp.cmi +boxPp.cmx: ast2pres.cmx box.cmx cicAstPp.cmx boxPp.cmi +tacticAst2Box.cmo: ast2pres.cmi box.cmi boxPp.cmi cicAstPp.cmi tacticAst.cmo \ + tacticAstPp.cmi tacticAst2Box.cmi +tacticAst2Box.cmx: ast2pres.cmx box.cmx boxPp.cmx cicAstPp.cmx tacticAst.cmx \ + tacticAstPp.cmx tacticAst2Box.cmi diff --git a/helm/ocaml/cic_transformations/Makefile b/helm/ocaml/cic_transformations/Makefile index ac8714e55..3c43c338d 100644 --- a/helm/ocaml/cic_transformations/Makefile +++ b/helm/ocaml/cic_transformations/Makefile @@ -15,7 +15,7 @@ INTERFACE_FILES = \ cicAstPp.mli ast2pres.mli content2pres.mli \ sequent2pres.mli \ misc.mli xml2Gdome.mli sequentPp.mli \ - applyStylesheets.mli applyTransformation.mli \ + applyTransformation.mli \ tacticAstPp.mli boxPp.mli tacticAst2Box.mli IMPLEMENTATION_FILES = \ tacticAst.ml \ diff --git a/helm/ocaml/cic_transformations/applyStylesheets.ml b/helm/ocaml/cic_transformations/applyStylesheets.ml deleted file mode 100644 index 72f39ea4d..000000000 --- a/helm/ocaml/cic_transformations/applyStylesheets.ml +++ /dev/null @@ -1,175 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 30/01/2002 *) -(* *) -(* *) -(******************************************************************************) - -(** stylesheets and parameters list **) - -let parseStyle name = - let style = - Misc.domImpl#createDocumentFromURI - (* ~uri:("http://phd.cs.unibo.it:8081/getxslt?uri=" ^ name) ?mode:None *) - ~uri:("styles/" ^ name) () - in - Gdome_xslt.processStylesheet style -;; - -let parseStyles () = - parseStyle "drop_coercions.xsl", - parseStyle "objtheorycontent.xsl", - parseStyle "content_to_html.xsl", - parseStyle "link.xsl", - parseStyle "rootcontent.xsl", - parseStyle "genmmlid.xsl", - parseStyle "annotatedpres.xsl" -;; - -let (d_c,tc1,hc2,l,c1,g,c2) = - let (d_c,tc1,hc2,l,c1,g,c2) = parseStyles () in - ref d_c, ref tc1, ref hc2, ref l, ref c1, ref g, ref c2 -;; - -let reload_stylesheets () = - let (d_c',tc1',hc2',l',c1',g',c2') = parseStyles () in - d_c := d_c'; - tc1 := tc1'; - hc2 := hc2'; - l := l' ; - c1 := c1' ; - g := g' ; - c2 := c2' -;; - - -let mml_styles = [d_c ; c1 ; g ; c2 ; l];; -let mml_args ~explode_all = - ("explodeall",(if explode_all then "true()" else "false()")):: - ["processorURL", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ; - "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'yes'" ; - "annotations", "'no'" ; - "URLs_or_URIs", "'URIs'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -let sequent_styles = [d_c ; c1 ; g ; c2 ; l];; -let sequent_args () = - ["processorURL", "'" ^ Helm_registry.get "uwobo.url" ^ "'" ; - "getterURL", "'" ^ Helm_registry.get "getter.url" ^ "'" ; - "draw_graphURL", "'http%3A//phd.cs.unibo.it%3A8083/'" ; - "uri_set_queueURL", "'http%3A//phd.cs.unibo.it%3A8084/'" ; - "UNICODEvsSYMBOL", "'symbol'" ; - "doctype-public", "'-//W3C//DTD%20XHTML%201.0%20Transitional//EN'" ; - "encoding", "'iso-8859-1'" ; - "media-type", "'text/html'" ; - "keys", "'d_c%2CC1%2CG%2CC2%2CL'" ; - "interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ; - "naturalLanguage", "'no'" ; - "annotations", "'no'" ; - "explodeall", "true()" ; - "URLs_or_URIs", "'URIs'" ; - "topurl", "'http://phd.cs.unibo.it/helm'" ; - "CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ] -;; - -(** Stylesheets application **) - -let apply_stylesheets input styles args = - List.fold_left (fun i style -> Gdome_xslt.applyStylesheet i !style args) - input styles -;; - -let apply_proof_stylesheets proof_doc ~explode_all = - apply_stylesheets proof_doc mml_styles (mml_args ~explode_all) -;; - -let apply_sequent_stylesheets sequent_doc = - apply_stylesheets sequent_doc sequent_styles (sequent_args ()) -;; - -(** Utility functions to map objects to MathML Presentation **) - -(*CSC: the getter should handle the innertypes, not the FS *) - -let innertypesfile () = Helm_registry.get "gtoplevel.inner_types_file";; -let constanttypefile () = Helm_registry.get "gtoplevel.constant_type_file";; - -let mml_of_cic_sequent metasenv sequent = - let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses = - SequentPp.XmlPp.print_sequent metasenv sequent in - let sequent_doc = - Xml2Gdome.document_of_xml Misc.domImpl sequent_gdome in - let sequent_mml = apply_sequent_stylesheets sequent_doc in - sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) -;; - -let - mml_of_cic_object ~explode_all uri annobj ids_to_inner_sorts ids_to_inner_types -= -(*CSC: ????????????????? *) - let xml, bodyxml = - Cic2Xml.print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter:true - annobj - in - let xmlinnertypes = - Cic2Xml.print_inner_types uri ~ids_to_inner_sorts ~ids_to_inner_types - ~ask_dtd_to_the_getter:true - in - let input = - match bodyxml with - None -> Xml2Gdome.document_of_xml Misc.domImpl xml - | Some bodyxml' -> - Xml.pp xml (Some (constanttypefile ())) ; - Xml2Gdome.document_of_xml Misc.domImpl bodyxml' - in -(*CSC: We save the innertypes to disk so that we can retrieve them in the *) -(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *) -(*CSC: local. *) - Xml.pp xmlinnertypes (Some (innertypesfile ())) ; - let output = apply_proof_stylesheets input ~explode_all in - output -;; - - - - - diff --git a/helm/ocaml/cic_transformations/applyStylesheets.mli b/helm/ocaml/cic_transformations/applyStylesheets.mli deleted file mode 100644 index c445d3708..000000000 --- a/helm/ocaml/cic_transformations/applyStylesheets.mli +++ /dev/null @@ -1,51 +0,0 @@ -(* Copyright (C) 2000-2002, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 15/01/2003 *) -(* *) -(* *) -(******************************************************************************) - -val reload_stylesheets : unit -> unit - -val mml_of_cic_sequent : - Cic.metasenv -> - int * Cic.context * Cic.term -> - Gdome.document * - ((Cic.id, Cic.term) Hashtbl.t * - (Cic.id, Cic.id option) Hashtbl.t * - (string, Cic.hypothesis) Hashtbl.t) - -val mml_of_cic_object : - explode_all:bool -> - UriManager.uri -> - Cic.annobj -> - (string, string) Hashtbl.t -> - (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 1b4e906e0..f0bda3261 100644 --- a/helm/ocaml/cic_transformations/tacticAst.ml +++ b/helm/ocaml/cic_transformations/tacticAst.ml @@ -90,6 +90,8 @@ type 'term inductive_type = string * bool * 'term * (string * 'term) list type search_kind = [ `Locate | `Hint | `Match | `Elim ] +type print_kind = [ `Env ] + type 'term command = | Abort | Baseuri of string option (** get/set base uri *) @@ -114,6 +116,7 @@ type 'term command = | Coercion of 'term | Redo of int option | Undo of int option + | Print of print_kind type ('term, 'ident) tactical = | LocatedTactical of CicAst.location * ('term, 'ident) tactical diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml index e01f28eb3..e256a19b8 100644 --- a/helm/ocaml/cic_unification/coercGraph.ml +++ b/helm/ocaml/cic_unification/coercGraph.ml @@ -196,7 +196,7 @@ let close_coercion_graph src tgt uri = (* stupid case *) - +(* let l = close_coercion_graph (UriManager.uri_of_string "cic:/CoRN/algebra/CRings/CRing.ind#xpointer(1/1)") @@ -210,7 +210,7 @@ in prerr_endline (UriManager.string_of_uri u); prerr_endline "") l - +*) (* EOF *) -- 2.39.2