metavariable context has a separator now

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index dbdb1530f8bd46c6f000b707df82652391633832..68afd810b6c8f3c0c0aa1d4222dc391602aaafc9 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
            ) branches
          else
-         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+         match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
             Cic.InductiveDefinition (il,_,leftsno,_) ->
              let _,_,_,cl =
               try
@@ -345,13 +345,13 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.LetIn ((name, typ), def, body) ->
         let cic_def = aux ~localize loc context def in
         let cic_name = CicNotationUtil.cic_name_of_name name in
-        let cic_def =
+        let cic_typ =
           match typ with
-          | None -> cic_def
-          | Some t -> Cic.Cast (cic_def, aux ~localize loc context t)
+          | None -> Cic.Implicit (Some `Type)
+          | Some t -> aux ~localize loc context t
         in
         let cic_body = aux ~localize loc (cic_name :: context) body in
-        Cic.LetIn (cic_name, cic_def, cic_body)
+        Cic.LetIn (cic_name, cic_def, cic_typ, cic_body)
     | CicNotationPt.LetRec (kind, defs, body) ->
         let context' =
           List.fold_left
@@ -380,6 +380,8 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
+                     (* since we avoid the letin, the context has no
+                      * recfuns in it *)
                      let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
@@ -431,9 +433,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                Cic.CoFix (n,coinductiveFuns)
         in
          let counter = ref ~-1 in
-         let build_term funs (var,_,_,_) t =
+         let build_term funs (var,_,ty,_) t =
           incr counter;
-          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, t)
+          Cic.LetIn (Cic.Name var, fix_or_cofix !counter, ty, t)
          in
           (match cic_body with
               `AvoidLetInNoAppl n ->
@@ -484,16 +486,16 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
           (try 
             match cic with
             | Cic.Const (uri, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                (try
-                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                  let uris = CicUtil.params_of_obj o in
                  Cic.MutInd (uri, i, mk_subst uris)
                 with
@@ -506,7 +508,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                   (*here the explicit_named_substituion is assumed to be of length 0 *)
                   Cic.MutInd (uri,i,[]))
             | Cic.MutConstruct (uri, i, j, []) ->
-                let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+                let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
                 let uris = CicUtil.params_of_obj o in
                 Cic.MutConstruct (uri, i, j, mk_subst uris)
             | Cic.Meta _ | Cic.Implicit _ as t ->
@@ -540,7 +542,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
-    | CicNotationPt.Sort `CProp -> Cic.Sort Cic.CProp
+    | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         resolve env (Symbol (symbol, instance)) ()
     | _ -> assert false (* god bless Bologna *)
@@ -785,6 +787,7 @@ let rec domain_of_term ?(loc = HExtlib.dummy_floc) ~context = function
                   CicNotationUtil.cic_name_of_name var :: context,
                   domain_of_term_option ~loc ~context ty @ res)
                 (add_defs context,[]) params))
+            @ dom
             @ domain_of_term_option ~loc ~context:context' typ
             @ domain_of_term ~loc ~context:context' body
           ) [] defs
@@ -976,7 +979,7 @@ module Make (C: Callbacks) =
 let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
 
     let disambiguate_thing ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
       (thing_txt,thing_txt_prefix_len,thing)
     =
@@ -1276,7 +1279,7 @@ in refine_profiler.HExtlib.profile foo ()
         failwith "Disambiguate: circular dependency"
 
     let disambiguate_term ?(fresh_instances=false) ~dbd ~context ~metasenv
-      ?(initial_ugraph = CicUniv.empty_ugraph) ~aliases ~universe 
+      ?(initial_ugraph = CicUniv.oblivion_ugraph) ~aliases ~universe 
       (text,prefix_len,term)
     =
       let term =