- ported to typed explicit substitutions

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 4b8099fed004c7e92ab152f190b5ca5599fde050..f5684a9510196194727e7a9e48bc9aaf2954146d 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -544,7 +544,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           )
      | (k, e, ens, (C.Meta (n,l) as t), s) ->
         (try 
-          let (_, term) = CicUtil.lookup_subst n subst in
+          let (_, term,_) = CicUtil.lookup_subst n subst in
            reduce (k, e, ens,CicSubstitution.lift_meta l term,s)
         with  CicUtil.Subst_not_found _ ->
            let t' = unwind k e ens t in

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 5715778fb07cd91ba54ce9cc1ca5b180374fb4fc..414d0b976a316f9168d8aaca09d9035d3eef352a 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -1330,19 +1330,9 @@ and check_metasenv_consistency ?(subst=[]) metasenv context canonical_context l
              let type_t = type_of_aux' ~subst metasenv context t in
              if not (R.are_convertible ~subst ~metasenv context type_t ct) then
               (* debug *)
-              (
-                 (*
-                (match type_t with 
-                    Cic.Meta (n,l) ->
-                      try 
-                        let (cc, ecco) = CicUtil.lookup_subst n subst in
-                        prerr_endline (CicPp.ppterm ecco)
-                      with CicUtil.Subst_not_found _ ->
-                         prerr_endline "Non lo trovo"
-                   | _ -> ()); *)
               raise (TypeCheckerFailure (sprintf
                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
-                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t))))
+                (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
          | None, _  ->
              raise (TypeCheckerFailure
               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
@@ -1379,15 +1369,17 @@ and type_of_aux' ?(subst = []) metasenv context t =
        ty
     | C.Meta (n,l) -> 
        (try
-          let (canonical_context, term) = CicUtil.lookup_subst n subst in
+          let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
           check_metasenv_consistency 
            ~subst metasenv context canonical_context l;
-          type_of_aux context (CicSubstitution.lift_meta l term)
+          (* assuming subst is well typed !!!!! *)
+          CicSubstitution.lift_meta l ty
+          (* type_of_aux context (CicSubstitution.lift_meta l term) *)
        with CicUtil.Subst_not_found _ ->
          let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
-            check_metasenv_consistency 
-             ~subst metasenv context canonical_context l;
-            CicSubstitution.lift_meta l ty)
+          check_metasenv_consistency 
+            ~subst metasenv context canonical_context l;
+          CicSubstitution.lift_meta l ty)
       (* TASSI: CONSTRAINTS *)
     | C.Sort (C.Type t) -> 
        let t' = CicUniv.fresh() in