- xml exportation activated for the brg kernel

[helm.git] / helm / software / components / ng_cic_content / nTermCicContent.ml

diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml
index 8984a4829547fc241d94a2ce90487b7565b3cbf8..c53a4a31c6ad0b7603f4dc8497323889012ea5c8 100644 (file)
--- a/helm/software/components/ng_cic_content/nTermCicContent.ml
+++ b/helm/software/components/ng_cic_content/nTermCicContent.ml
@@ -93,7 +93,8 @@ let nast_of_cic0 status
        F.fprintf f ")"*)
     (* CSC: qua siamo grezzi *)
     | NCic.Implicit `Hole -> idref (Ast.UserInput)
-    | NCic.Implicit _ -> idref (Ast.Implicit)
+    | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
+    | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
     | NCic.Prod (n,s,t) ->
         let n = if n.[0] = '_' then "_" else n in
         let binder_kind = `Forall in
@@ -153,7 +154,7 @@ let nast_of_cic0 status
        let rec eat_branch n ctx ty pat =
           match (ty, pat) with
          | NCic.Prod (name, s, t), _ when n > 0 ->
-             eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat 
+             eat_branch (pred n) ctx t pat 
           | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
               let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
               (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs