Fixed a few bugs in the inference of the outtype for a match.

In particular the instances of the left parameter that occur in the
outtype were not lifted properly because of the abstractions that correspond
to the right parameters.

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 351104f56f7806917a9e4a89ea6b92ef3ed7b8d4..8828a417e5272c4cbb2731dcd3cde150e0342212 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -460,9 +460,13 @@ and type_of_aux' metasenv context t ugraph =
                        function
                           0 -> []
                         | n -> (Cic.Rel n)::(mk_right_args (n - 1))
+                      in
+                      let right_args_no = List.length right_args in
+                      let lifted_left_args =
+                       List.map (CicSubstitution.lift right_args_no) left_args
                       in
                        Cic.Appl (Cic.MutInd(uri,i,exp_name_subst)::
-                        (left_args @ mk_right_args (List.length right_args)))
+                        (lifted_left_args @ mk_right_args right_args_no))
                  in
                  let fresh_name = 
                    FreshNamesGenerator.mk_fresh_name ~subst metasenv 
@@ -471,13 +475,16 @@ and type_of_aux' metasenv context t ugraph =
                  match outtypeinstances with
                  | [] -> 
                      let extended_context = 
-                      let rec add_right_args b =
+                      let rec add_right_args =
                        function
                           Cic.Prod (name,ty,t) ->
-                           Some (name,Cic.Decl ty)::(add_right_args b t)
-                        | _ -> (Some (fresh_name,Cic.Decl ty))::b
+                           Some (name,Cic.Decl ty)::(add_right_args t)
+                        | _ -> []
                       in
-                       add_right_args context arity_instantiated_with_left_args
+                       (Some (fresh_name,Cic.Decl ty))::
+                       (List.rev
+                        (add_right_args arity_instantiated_with_left_args))@
+                       context
                      in
                      let metasenv,new_meta = 
                        CicMkImplicit.mk_implicit metasenv subst extended_context