From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 5 Jul 2005 15:08:10 +0000 (+0000)
Subject: Bug fixed: the outtype of a match when omitted was interpreted as an implicit
X-Git-Tag: V_0_7_1~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc690e0dfa17463d516b74d0a7e5aad810ee1b41;p=helm.git

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 6b5e3f833..9896db7c9 100644
--- 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