From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 15 Apr 2008 08:20:24 +0000 (+0000)
Subject: do not use an implicit but a sort as a neutral term for positivity check
X-Git-Tag: make_still_working~5338
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3270d5e228bbcd3dfe7350e59416b843a5149e3b;p=helm.git

do not use an implicit but a sort as a neutral term for positivity check
---

diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml
index 334ab8622..26e2163ea 100644
--- a/helm/software/components/ng_kernel/nCicTypeChecker.ml
+++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml
@@ -417,29 +417,30 @@ let does_not_occur ~subst context n nn t =
 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 let rec weakly_positive ~subst context n nn uri te =
 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
-  let dummy_mutind = C.Implicit `Hole in
+  let dummy = C.Sort (C.Type ~-1) in
   (*CSC: mettere in cicSubstitution *)
-  let rec subst_inductive_type_with_dummy_mutind _ = function
-    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy_mutind
-    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) when NUri.eq uri' uri ->
-       dummy_mutind
-    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy_mutind t
+  let rec subst_inductive_type_with_dummy _ = function
+    | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
+    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl) 
+        when NUri.eq uri' uri -> dummy
+    | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
   in
   match R.whd context te with
    | C.Const (Ref.Ref (_,uri',Ref.Ind _))
-   | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) when NUri.eq uri' uri -> true
+   | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_) 
+      when NUri.eq uri' uri -> true
    | C.Prod (name,source,dest) when
       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
        (* dummy abstraction, so we behave as in the anonimous case *)
        strictly_positive ~subst context n nn
-        (subst_inductive_type_with_dummy_mutind () source) &&
-         weakly_positive ~subst ((name,C.Decl source)::context)
-         (n + 1) (nn + 1) uri dest
+        (subst_inductive_type_with_dummy () source) &&
+       weakly_positive ~subst ((name,C.Decl source)::context)
+        (n + 1) (nn + 1) uri dest
    | C.Prod (name,source,dest) ->
        does_not_occur ~subst context n nn
-         (subst_inductive_type_with_dummy_mutind () source)&&
-         weakly_positive ~subst ((name,C.Decl source)::context)
-         (n + 1) (nn + 1) uri dest
+        (subst_inductive_type_with_dummy () source)&&
+       weakly_positive ~subst ((name,C.Decl source)::context)
+        (n + 1) (nn + 1) uri dest
    | _ ->
      raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))