differentieted empty substitution list from no substitution given

diff --git a/helm/ocaml/cic_transformations/acic2Ast.ml b/helm/ocaml/cic_transformations/acic2Ast.ml
index 19b6c4b4bf4161ab4546d2f178fe9e13d2c117be..e51e9c0a401b3d69accb7790a364e6243ab12836 100644 (file)
--- a/helm/ocaml/cic_transformations/acic2Ast.ml
+++ b/helm/ocaml/cic_transformations/acic2Ast.ml
@@ -70,7 +70,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
   let module Ast = CicAst in
   let idref id t = Ast.AttributedTerm (`IdRef id, t) in
   let rec aux = function
-    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, []))
+    | Cic.ARel (id,_,_,b) -> idref id (Ast.Ident (b, None))
     | Cic.AVar (id,uri,subst) ->
         register_uri id (UriManager.string_of_uri uri);
         idref id
@@ -181,7 +181,7 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -195,11 +195,13 @@ let ast_of_acic ids_to_inner_sorts ids_to_uris acic =
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, [])))
+        idref id (Ast.LetRec (`CoInductive, defs, Ast.Ident (name, None)))
 
   and astsubst_of_cicsubst subst =
-    List.map (fun (uri, annterm) -> (UriManager.name_of_uri uri, aux annterm))
-      subst
+    Some
+      (List.map (fun (uri, annterm) ->
+        (UriManager.name_of_uri uri, aux annterm))
+        subst)
 
   and astcontext_of_ciccontext context =
     List.map

diff --git a/helm/ocaml/cic_transformations/ast2pres.ml b/helm/ocaml/cic_transformations/ast2pres.ml
index 9679501ab460d2c8ae707edfbc36db396037ac22..dbbfff8e5e0432b2ce9e5064abbdeabf151df217 100644 (file)
--- a/helm/ocaml/cic_transformations/ast2pres.ml
+++ b/helm/ocaml/cic_transformations/ast2pres.ml
@@ -76,7 +76,8 @@ and countterm current_size t =
                let size1 = countvar c var in
                countterm size1 s) current_size l in
          countterm size1 t
-    | A.Ident(s,l) ->
+    | A.Ident(s,None) -> current_size + (String.length s)
+    | A.Ident(s,Some l) ->
         List.fold_left 
          (fun c (v,t) -> countterm (c + (String.length v)) t) 
           (current_size + (String.length s)) l
@@ -218,8 +219,12 @@ and bigast2box ?(priority = 0) ?(assoc = false) ?(attr = []) =
            | [(s,t)] -> 
                make_subst start_txt s t "]"
            | (s,t)::tl ->
-               (make_subst start_txt s t ";")@(make_substs " " tl) in
-         make_substs "[" subst in
+               (make_subst start_txt s t ";")@(make_substs " " tl)
+          in
+          match subst with
+          | Some subst -> make_substs "[" subst
+          | None -> []
+        in
        Box.V([], (* attr here or on Vbox? *)
              [Box.Text(map_attributes attr,s);
               Box.indent(Box.V([],subst))])

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 92ab328c18a1e9ac16881d5d7815da2664cd9a68..f7392fa3ac34bdfe8c4423902cd54a4c4c15fb06 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -44,7 +44,10 @@ type term =
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term
       (* (name, body, decreasing argument) list, where *)
-  | Ident of string * subst list  (* literal, substitutions *)
+  | Ident of string * subst list option
+      (* literal, substitutions.
+      * Some [] -> user has given an empty explicit substitution list 
+      * None -> user has given no explicit substitution list *)
   | Implicit
   | Meta of int * meta_subst list
   | Num of string * int (* literal, instance *)

diff --git a/helm/ocaml/cic_transformations/cicAstPp.ml b/helm/ocaml/cic_transformations/cicAstPp.ml
index 02cf5511cd963a07b84c4c65b3902b0fde0f62fb..bd9eea6012927c97c6a64f0cb8fdf8d8483a6117 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAstPp.ml
+++ b/helm/ocaml/cic_transformations/cicAstPp.ml
@@ -62,8 +62,10 @@ let rec pp_term = function
               sprintf "%s = %s" (pp_capture_variable var) (pp_term body))
             definitions))
         (pp_term term)
-  | CicAst.Ident (name, []) -> name
-  | CicAst.Ident (name, substs) -> sprintf "%s[%s]" name (pp_substs substs)
+  | CicAst.Ident (name, Some [])
+  | CicAst.Ident (name, None) ->
+      name
+  | CicAst.Ident (name, Some substs) -> sprintf "%s[%s]" name (pp_substs substs)
   | CicAst.Implicit -> "?"
   | CicAst.Meta (index, substs) ->
       sprintf "%d[%s]" index