**** Experimental: ****

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 026f9ebd1ee238ad6e7b7de248fa2f4f415bec30..c33462f8fd90269eedabefac815c2af3f6c1c5c2 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -822,9 +822,13 @@ module Make (C: Callbacks) =
         let res =
          match aux current_env todo_dom base_univ with
          | [] -> raise NoWellTypedInterpretation
-         | [ e,me,t,u ] as l ->
+         | [ e,me,t,u ] ->
              debug_print "UNA SOLA SCELTA";
-             [ e,me,t,u]
+             (* Experimental: we forget the environment [e] since we are able
+                to recompute it. In this way we are forced to do more work
+                later (since we have less aliases), but we have more freedom
+                (since we have less aliases) in the future disambiguations. *)
+             [ current_env,me,t,u]
          | l ->
              debug_print (sprintf "PIU' SCELTE (%d)" (List.length l));
              let choices =