Bug fixed: the outtype of a match when omitted was interpreted as an implicit

type (instead it is an implicit term). Thus its type was restricted to be a
sort.

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 6b5e3f8332c60e21283486461032d020f12ac60d..9896db7c91ace4970253a72f9db435aff45bea52 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -35,7 +35,7 @@ exception PathNotWellFormed
   (** raised when an environment is not enough informative to decide *)
 exception Try_again
 
-let debug = false
+let debug = true
 let debug_print = if debug then prerr_endline else ignore
 
 (*
@@ -119,7 +119,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
         resolve env (Symbol (symb, i)) ~args:cic_args ()
     | CicAst.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
     | CicAst.Binder (binder_kind, (var, typ), body) ->
-        let cic_type = aux_option loc context typ in
+        let cic_type = aux_option loc context (Some `Type) typ in
         let cic_body = aux loc (var :: context) body in
         (match binder_kind with
         | `Lambda -> Cic.Lambda (var, cic_type, cic_body)
@@ -129,7 +129,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
               ~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
     | CicAst.Case (term, indty_ident, outtype, branches) ->
         let cic_term = aux loc context term in
-        let cic_outtype = aux_option loc context outtype in
+        let cic_outtype = aux_option loc context None outtype in
         let do_branch ((head, args), term) =
           let rec do_branch' context = function
             | [] -> aux loc context term
@@ -184,7 +184,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           List.map
             (fun ((name, typ), body, decr_idx) ->
               let cic_body = aux loc context' body in
-              let cic_type = aux_option loc context typ in
+              let cic_type = aux_option loc context (Some `Type) typ in
               let name =
                 match name with
                 | Cic.Anonymous ->
@@ -311,8 +311,8 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
     | CicAst.Sort `CProp -> Cic.Sort Cic.CProp
     | CicAst.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
-  and aux_option loc context = function
-    | None -> Cic.Implicit (Some `Type)
+  and aux_option loc context annotation = function
+    | None -> Cic.Implicit annotation
     | Some term -> aux loc context term
   in
   match ast with