diff options
| author | herbelin | 2003-09-06 19:12:08 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-06 19:12:08 +0000 |
| commit | 95d4aef96fb7b490b188afe66e8345428e9706ee (patch) | |
| tree | 3990c1a6bfce095e941d756df5387b63e86e8353 /contrib/xml | |
| parent | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (diff) | |
Paramétrisation vis à vis de existential_key
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml')
| -rw-r--r-- | contrib/xml/acic.ml | 6 | ||||
| -rw-r--r-- | contrib/xml/acic2Xml.ml4 | 7 |
2 files changed, 8 insertions, 5 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml index 693b7cb3c8..36541a57df 100644 --- a/contrib/xml/acic.ml +++ b/contrib/xml/acic.ml @@ -23,7 +23,7 @@ type 'constr context_entry = type 'constr hypothesis = identifier * 'constr context_entry type context = constr hypothesis list -type conjecture = int * context * constr +type conjecture = existential_key * context * constr type metasenv = conjecture list (* list of couples section path -- variables defined in that section *) @@ -51,7 +51,7 @@ and constructor = type aconstr = | ARel of id * int * id * identifier | AVar of id * uri - | AEvar of id * int * aconstr list + | AEvar of id * existential_key * aconstr list | ASort of id * sorts | ACast of id * aconstr * aconstr | AProds of (id * name * aconstr) list * aconstr @@ -71,7 +71,7 @@ and acoinductivefun = and explicit_named_substitution = id option * (uri * aconstr) list type acontext = (id * aconstr hypothesis) list -type aconjecture = id * int * acontext * aconstr +type aconjecture = id * existential_key * acontext * aconstr type ametasenv = aconjecture list type aobj = diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4 index b70ede2d8e..4e64ca5d15 100644 --- a/contrib/xml/acic2Xml.ml4 +++ b/contrib/xml/acic2Xml.ml4 @@ -37,6 +37,8 @@ let rec find_last_id = | _::tl -> find_last_id tl ;; +let export_existential = string_of_int + let print_term ids_to_inner_sorts = let rec aux = let module A = Acic in @@ -53,7 +55,8 @@ let print_term ids_to_inner_sorts = X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] | A.AEvar (id,n,l) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] + X.xml_nempty "META" + ["no",(export_existential n) ; "id",id ; "sort",sort] (List.fold_left (fun i t -> [< i ; X.xml_nempty "substitution" [] (aux t) >] @@ -231,7 +234,7 @@ let print_object uri ids_to_inner_sorts = (fun i (cid,n,canonical_context,t) -> [< i ; X.xml_nempty "Conjecture" - ["id", cid ; "no",(string_of_int n)] + ["id", cid ; "no",export_existential n] [< List.fold_left (fun i (hid,t) -> [< (match t with |