Revert specific syntax for primitive projections, avoiding ugly

contortions in internalization/externalization. It uses a fully typed
version of detyping, requiring the environment, to move from
primitive projection applications to regular applications of
the eta-expanded version. The kernel is unchanged, and only
constrMatching needs compatibility code now.

5 files changed, 25 insertions, 44 deletions

diff --git a/test-suite/bugs/closed/3454.v b/test-suite/bugs/closed/3454.v
index 43108ab4b..ca4d23803 100644
--- a/test-suite/bugs/closed/3454.v
+++ b/test-suite/bugs/closed/3454.v
@@ -1,8 +1,11 @@
 Set Primitive Projections.
 Set Implicit Arguments.
+
+Record prod {A} {B}:= pair { fst : A ; snd : B }.
+Notation " A * B " := (@prod A B) : type_scope.
 Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
 Notation pr1 := (@projT1 _ _).
-
+Arguments prod : clear implicits.
 
 Check (@projT1 _ (fun x : nat => x = x)).
 Check (fun s : @sigT nat (fun x : nat => x = x) => s.(projT1)).
@@ -13,7 +16,7 @@ Check (fun r : @rimpl true 0 => r.(foo) (x:=0)).
 Check (fun r : @rimpl true 0 => @foo true 0 r 0).
 Check (fun r : @rimpl true 0 => foo r (x:=0)).
 Check (fun r : @rimpl true 0 => @foo _ _ r 0).
-Check (fun r : @rimpl true 0 => r.(@foo)).
+Check (fun r : @rimpl true 0 => r.(@foo _ _)).
 Check (fun r : @rimpl true 0 => r.(foo)).
 
 Notation "{ x : T  & P }" := (@sigT T P).
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
index b47bb3a20..c68796593 100644
--- a/test-suite/bugs/closed/HoTT_coq_054.v
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-emacs") -*- *)
 Inductive Empty : Prop := .
 
 Inductive paths {A : Type} (a : A) : A -> Type :=
@@ -47,10 +47,10 @@ Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
                          | inl y' => ap g
                          | inr y' => idmap
                        end
-           | inr x' => match y as y return match y return Type with
+           | inr x' => match y as y return match y return Prop with
                                                inr y' => x' = y'
                                              | _ => Empty
-                                           end -> match f y return Type with
+                                           end -> match f y return Prop with
                                                     | inr y' => h x' = y'
                                                     | _ => Empty end with
                          | inl y' => idmap
diff --git a/test-suite/bugs/closed/HoTT_coq_108.v b/test-suite/bugs/closed/HoTT_coq_108.v
index 77f921b7c..cc3048027 100644
--- a/test-suite/bugs/closed/HoTT_coq_108.v
+++ b/test-suite/bugs/closed/HoTT_coq_108.v
@@ -115,7 +115,7 @@ Section path_functor.
   Proof.
     intros [H' H''].
     destruct F, G; simpl in *.
-    induction H'; induction H''; simpl.
+    induction H'. (* while destruct H' works *) destruct H''.
     apply ap11; [ apply ap | ];
     apply center; abstract exact _.
     Set Printing Universes.
diff --git a/test-suite/bugs/opened/HoTT_coq_083.v b/test-suite/bugs/opened/HoTT_coq_083.v
deleted file mode 100644
index 091720272..000000000
--- a/test-suite/bugs/opened/HoTT_coq_083.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Set Primitive Projections.
-Set Implicit Arguments.
-Set Universe Polymorphism.
-
-Record category :=
-  { ob : Type }.
-
-Goal forall C, ob C -> ob C.
-intros.
-generalize dependent (ob C).
-(* 1 subgoals, subgoal 1 (ID 7)
-
-  C : category
-  ============================
-   forall T : Type, T -> T
-(dependent evars:) *)
-intros T t.
-Undo 2.
-generalize dependent (@ob C).
-(* 1 subgoals, subgoal 1 (ID 6)
-
-  C : category
-  X : ob C
-  ============================
-   Type -> ob C
-(dependent evars:) *)
-Fail intros T t.
-(* Toplevel input, characters 9-10:
-Error: No product even after head-reduction. *)
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 74083ac89..068f8ac3c 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -115,22 +115,22 @@ Unset Printing All.
 
 (** Explicit version of the primitive projection, under applied w.r.t implicit arguments
       can be printed only using projection notation. r.(@p) *)
-Check r.(@p). 
+Check r.(@p _). 
 Set Printing Projections.
-Check r.(@p). 
+Check r.(@p _). 
 Unset Printing Projections.
 Set Printing All.
-Check r.(@p).
+Check r.(@p _).
 Unset Printing All.
   
 (** Explicit version of the primitive projection, applied to its implicit arguments
       can be printed using application notation r.(p), r.(@p) in fully explicit form *)
-Check r.(@p) nat.
+Check r.(@p _) nat.
 Set Printing Projections.
-Check r.(@p) nat. 
+Check r.(@p _) nat. 
 Unset Printing Projections.
 Set Printing All.
-Check r.(@p) nat.
+Check r.(@p _) nat.
 Unset Printing All.
 
 Parameter r' : R' nat.
@@ -163,12 +163,12 @@ Unset Printing All.
 
 (** Explicit version of the primitive projection, under applied w.r.t implicit arguments
       can be printed only using projection notation. r.(@p) *)
-Check r'.(@p'). 
+Check r'.(@p' _). 
 Set Printing Projections.
-Check r'.(@p'). 
+Check r'.(@p' _). 
 Unset Printing Projections.
 Set Printing All.
-Check r'.(@p').
+Check r'.(@p' _).
 Unset Printing All.
   
 (** Explicit version of the primitive projection, applied to its implicit arguments
@@ -181,3 +181,10 @@ Set Printing All.
 Check p' r' nat. 
 Unset Printing All.
 
+Check (@p' nat).
+Check p'.
+Set Printing All.
+
+Check (@p' nat).
+Check p'.
+Unset Printing All.