split into two major parts:

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f753b30ae714d724df1968653b0c4c14ba6f10ac..110f3d75ea1578b8f5ae2eb7735a48e61147eeae 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -102,7 +102,7 @@ let interpretate ~context ~env ast =
                 let cic_body = do_branch' (name :: context) tl in
                 let typ =
                   match typ with
-                  | None -> Cic.Implicit
+                  | None -> Cic.Implicit (Some `Type)
                   | Some typ -> aux loc context typ
                 in
                 Cic.Lambda (name, typ, cic_body)
@@ -112,7 +112,7 @@ let interpretate ~context ~env ast =
         let (indtype_uri, indtype_no) =
           match resolve env (Id indty_ident) () with
           | Cic.MutInd (uri, tyno, _) -> uri, tyno
-          | Cic.Implicit -> raise Try_again
+          | Cic.Implicit _ -> raise Try_again
           | _ -> raise DisambiguateChoices.Invalid_choice
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
@@ -175,7 +175,7 @@ let interpretate ~context ~env ast =
               "Explicit substitutions not allowed here";
           Cic.Rel index
         with Not_found -> resolve env (Id name) ())
-    | CicAst.Implicit -> Cic.Implicit
+    | CicAst.Implicit -> Cic.Implicit None
     | CicAst.Num (num, i) -> resolve env (Num i) ~num ()
     | CicAst.Meta (index, subst) ->
         let cic_subst =
@@ -191,12 +191,12 @@ let interpretate ~context ~env ast =
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
   and aux_option loc context = function
-    | None -> Cic.Implicit
+    | None -> Cic.Implicit (Some `Type)
     | Some term -> aux loc context term
   in
   match ast with
   | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | _ -> assert false
+  | term -> aux (-1, -1) context term
 
 let domain_of_term ~context ast =
     (* "aux" keeps domain in reverse order and doesn't care about duplicates.
@@ -293,9 +293,10 @@ let domain_of_term ~context ast =
       List.rev uniq_rev_l
   in
             
-  match ast with
-  | CicAst.AttributedTerm (`Loc loc, term) -> rev_uniq (aux loc context term)
-  | _ -> assert false
+  rev_uniq
+    (match ast with
+    | CicAst.AttributedTerm (`Loc loc, term) -> aux loc context term
+    | term -> aux (-1, -1) context term)
 
 
   (* dom1 \ dom2 *)
@@ -389,7 +390,11 @@ module Make (C: Callbacks) =
         let filled_env =
           List.fold_left
             (fun env item ->
-              Environment.add item ("Implicit", fun _ _ _ -> Cic.Implicit) env)
+              Environment.add item
+                ("Implicit",
+                 (match item with
+                 | Id _ | Num _ -> (fun _ _ _ -> Cic.Implicit (Some `Closed))
+                 | Symbol _ -> (fun _ _ _ -> Cic.Implicit None))) env)
             current_env todo_dom 
         in
         try