...

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 851cda9d2f3fc833853005c0af386cab1cc47311..6f1c9293a912f03a156b22a7819cf29377d71f0e 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -220,7 +220,7 @@ let _ =
             NCicMetaSubst.saturate ~delta:max_int [] ctx ty 0
           in
 *)
-          let ctx, ty = intros ty in
+(*           let ctx, ty = intros ty in *)
           let whd ty =
             match ty with
             | NCic.Appl [eq;t;a;b] ->
@@ -236,7 +236,7 @@ let _ =
           let metasenv, subst = 
             try 
 (*                     prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *)
-              NCicUnification.unify menv [] ctx ity sty
+              NCicUnification.unify menv [] ctx ity pty
             with
             | NCicUnification.Uncertain msg 
             | NCicUnification.UnificationFailure msg 
@@ -246,11 +246,11 @@ let _ =
                  (Printf.sprintf "RESULT OF UNIF\n%s\n%s == %s\n"
                  (NCicPp.ppcontext ~metasenv:menv ~subst:[] ctx)
                  (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx ity)
-                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx sty));
+                 (NCicPp.ppterm ~metasenv:menv ~subst:[] ~context:ctx pty));
                 [], []
             | Sys.Break -> [],[]
           in
-          if (NCicReduction.are_convertible ~subst ctx ity sty)
+          if (NCicReduction.are_convertible ~subst ctx ity pty)
           then
             prerr_endline ("OK: " ^ NUri.string_of_uri u)
           else

diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma
index 4005ee98ac2a187b441f06556473fbfbf3594579..e686e7eeef38c1669e74fe4b415de82c36091f8d 100644 (file)
--- a/helm/software/components/ng_refiner/esempio.ma
+++ b/helm/software/components/ng_refiner/esempio.ma
@@ -16,18 +16,6 @@ include "nat/plus.ma".
 
 definition hole : ∀A:Type.A → A ≝ λA.λx.x.
 
-inductive pippo (T:Type) (x:T) : Prop ≝ . 
-
-axiom A: Type. 
-axiom B:A.
-
-axiom foo : \forall x: (hole ? A).pippo (hole ? A) x.
-
-axiom foo: (λx,y:A. pippo (hole ? A) x y) 
-           (hole ? B) (hole ? B).
-
-axiom foo: λx:(hole ? Type).λy:(hole ? Type). pippo (hole ? Type) x y.
-
 axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) 
 axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *)